diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-20 14:02:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-20 14:02:58 +0000 |
| commit | 98f6a9d847f4fac14696f51096c8334c9bffda6f (patch) | |
| tree | 3ab3dabe0f93f38b17434976f0b0c9833b8e3ff5 /parsing/g_tactic.ml4 | |
| parent | fbcd19a076f255614012fd076863ca296c1b2626 (diff) | |
Only one "in" clause in "destruct" even for a multiple "destruct".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 32 |
1 files changed, 19 insertions, 13 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 81374e2f2..68e437cab 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -148,9 +148,9 @@ let induction_arg_of_constr (c,lbind as clbind) = else ElimOnConstr clbind let mkTacCase with_evar = function - | [([ElimOnConstr cl],None,(None,None),None)] -> + | [([ElimOnConstr cl],None,(None,None))],None -> TacCase (with_evar,cl) - | [([ElimOnIdent id],None,(None,None),None)] -> + | [([ElimOnIdent id],None,(None,None))],None -> TacCase (with_evar,(CRef (Ident id),NoBindings)) | ic -> TacInductionDestruct (false,with_evar,ic) @@ -462,7 +462,13 @@ GEXTEND Gram ; induction_clause: [ [ lc = LIST1 induction_arg; ipats = with_induction_names; - el = OPT eliminator; cl = opt_clause -> (lc,el,ipats,cl) ] ] + el = OPT eliminator -> (lc,el,ipats) ] ] + ; + one_induction_clause: + [ [ ic = induction_clause; cl = opt_clause -> ([ic],cl) ] ] + ; + induction_clause_list: + [ [ ic = LIST1 induction_clause SEP ","; cl = opt_clause -> (ic,cl) ] ] ; move_location: [ [ IDENT "after"; id = id_or_meta -> MoveAfter id @@ -500,8 +506,8 @@ GEXTEND Gram | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (true,cl,el) | IDENT "elimtype"; c = constr -> TacElimType c - | IDENT "case"; ic = LIST1 induction_clause SEP "," -> mkTacCase false ic - | IDENT "ecase"; ic = LIST1 induction_clause SEP "," -> mkTacCase true ic + | 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) @@ -556,18 +562,18 @@ GEXTEND Gram (* Derived basic tactics *) | IDENT "simple"; IDENT"induction"; h = quantified_hypothesis -> TacSimpleInductionDestruct (true,h) - | IDENT "induction"; ic = induction_clause -> - TacInductionDestruct (true,false,[ic]) - | IDENT "einduction"; ic = induction_clause -> - TacInductionDestruct(true,true,[ic]) + | IDENT "induction"; ic = one_induction_clause -> + TacInductionDestruct (true,false,ic) + | IDENT "einduction"; ic = one_induction_clause -> + TacInductionDestruct(true,true,ic) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) | IDENT "simple"; IDENT "destruct"; h = quantified_hypothesis -> TacSimpleInductionDestruct (false,h) - | IDENT "destruct"; ic = LIST1 induction_clause SEP "," -> - TacInductionDestruct(false,false,ic) - | IDENT "edestruct"; ic = LIST1 induction_clause SEP "," -> - TacInductionDestruct(false,true,ic) + | IDENT "destruct"; icl = induction_clause_list -> + TacInductionDestruct(false,false,icl) + | IDENT "edestruct"; icl = induction_clause_list -> + TacInductionDestruct(false,true,icl) | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = constr -> TacDecomposeOr c | IDENT "decompose"; "["; l = LIST1 smart_global; "]"; c = constr |