diff options
| author | Pierre-Marie Pédrot | 2014-05-18 02:50:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-20 14:49:47 +0200 |
| commit | e705ae9d343c67212ce238899d21059ce93ee3e5 (patch) | |
| tree | 33eb5575b2da7275fdb13295243ef045afab3375 /parsing | |
| parent | f79e9db4922f649d08153f09526d5c1c60a7e45c (diff) | |
Tentative to add constr-using primitive tactics without grammar rules.
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d1620ca8a7..4ac7a5bffe 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -533,8 +533,6 @@ GEXTEND Gram | IDENT "intro" -> TacIntroMove (None, MoveLast) | IDENT "exact"; c = constr -> TacExact c - | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c - | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","; inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp) @@ -548,10 +546,8 @@ GEXTEND Gram TacElim (false,cl,el) | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (true,cl,el) - | IDENT "elimtype"; c = constr -> TacElimType c | IDENT "case"; icl = induction_clause_list -> mkTacCase false icl | IDENT "ecase"; icl = induction_clause_list -> mkTacCase true icl - | IDENT "casetype"; c = constr -> TacCaseType c | "fix"; n = natural -> TacFix (None,n) | "fix"; id = ident; n = natural -> TacFix (Some id,n) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> @@ -587,7 +583,6 @@ GEXTEND Gram | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> TacAssert (None,ipat,c) - | IDENT "cut"; c = constr -> TacCut c | IDENT "generalize"; c = constr -> TacGeneralize [((AllOccurrences,c),Names.Anonymous)] | IDENT "generalize"; c = constr; l = LIST1 constr -> @@ -601,7 +596,6 @@ GEXTEND Gram | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings -> TacSpecialize (n,lcb) - | IDENT "lapply"; c = constr -> TacLApply c (* Derived basic tactics *) | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> |