forall fun fix cofix let in if then else match end Prop Set Type Axiom Conjecture Parameter Parameters Variable Variables Hypothesis Hypotheses Definition Let Inductive CoInductive with Fixpoint CoFixpoint Theorem Lemma Definition Print Term About All Check Eval Extraction Recursive Opaque Transparent Search SearchAbout SearchPattern SearchRewrite Locate Whelp Load Require Export Module Modules Section Qed Quit Pwd Cd Add LoadPath Remove do info progress try repeat fail let rec with match goal reverse lazymatch abstract first idtac solve fail fresh context eval type external constr exact eexact refine apply assumption auto clear move after until intro intros compute cbv lazy beta delta iota zeta Evar