diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 20 |
2 files changed, 18 insertions, 8 deletions
@@ -29,13 +29,15 @@ Tactics - New variant "subst'" of "subst" that supports JMeq. - New tactic "decide lemma with hyp" for rewriting decidability lemmas when one knows which side is true. -- Tactic "exists" and "eexists" supports iteration using - comma-separated arguments. +- Tactic "exists", "eexists", "destruct" and "edestruct" supports iteration + using comma-separated arguments. - Tactic "gappa" has been removed from the Dp plugin. - Tactic "firstorder" now supports the combination of its "using" and "with" options. - An inductive type as argument of the "using" option of "auto/eauto/firstorder" is interpreted as using the collection of its constructors. +- Tactic names "case" and "elim" now support clauses "as" and "in" and become + then synonymous of "destruct" and "induction" respectively. Tactic Language diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index c61bff02d7..81374e2f25 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -147,6 +147,14 @@ let induction_arg_of_constr (c,lbind as clbind) = with _ -> ElimOnConstr clbind else ElimOnConstr clbind +let mkTacCase with_evar = function + | [([ElimOnConstr cl],None,(None,None),None)] -> + TacCase (with_evar,cl) + | [([ElimOnIdent id],None,(None,None),None)] -> + TacCase (with_evar,(CRef (Ident id),NoBindings)) + | ic -> + TacInductionDestruct (false,with_evar,ic) + let rec mkCLambdaN_simple_loc loc bll c = match bll with | ((loc1,_)::_ as idl,bk,t) :: bll -> @@ -492,8 +500,8 @@ GEXTEND Gram | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (true,cl,el) | IDENT "elimtype"; c = constr -> TacElimType c - | IDENT "case"; cl = constr_with_bindings -> TacCase (false,cl) - | IDENT "ecase"; cl = constr_with_bindings -> TacCase (true,cl) + | IDENT "case"; ic = LIST1 induction_clause SEP "," -> mkTacCase false ic + | IDENT "ecase"; ic = LIST1 induction_clause SEP "," -> mkTacCase true ic | IDENT "casetype"; c = constr -> TacCaseType c | "fix"; n = natural -> TacFix (None,n) | "fix"; id = ident; n = natural -> TacFix (Some id,n) @@ -556,10 +564,10 @@ GEXTEND Gram h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis -> TacSimpleInductionDestruct (false,h) - | IDENT "destruct"; ic = induction_clause -> - TacInductionDestruct(false,false,[ic]) - | IDENT "edestruct"; ic = induction_clause -> - TacInductionDestruct(false,true,[ic]) + | IDENT "destruct"; ic = LIST1 induction_clause SEP "," -> + TacInductionDestruct(false,false,ic) + | IDENT "edestruct"; ic = LIST1 induction_clause SEP "," -> + TacInductionDestruct(false,true,ic) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr |