diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 17:31:59 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 17:31:59 +0000 |
| commit | e60fae1d7442c8662cdf3174590df972e7940635 (patch) | |
| tree | e9f35bde6fb63bd76e630f227ece58a66d27ebed /parsing/g_tacticnew.ml4 | |
| parent | 8a8b61d623dd1a37cf5a7edb4d77ba8cae893085 (diff) | |
Bug pattern_occ_hyp_list
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3818 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_tacticnew.ml4')
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 4083fe82c..dade80611 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -142,12 +142,16 @@ GEXTEND Gram pattern_occ: [ [ nl = LIST0 integer; c = [c=constr->c | g=global->Topconstr.CRef g]-> (nl,c) ] ] ; + pattern_occ_hyp_tail_list: + [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ] + ; pattern_occ_hyp_list: [ [ nl = LIST1 natural; IDENT "Goal" -> (Some nl,[]) - | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_list -> - (g,(id,nl)::l) + | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list + -> (g,(id,nl)::l) | IDENT "Goal" -> (Some [],[]) - | id = id_or_meta; (g,l) = pattern_occ_hyp_list -> (g,(id,[])::l) ] ] + | id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list -> (g,(id,[])::l) + ] ] ; clause_pattern: [ [ "in"; p = pattern_occ_hyp_list -> p | -> None, [] ] ] @@ -298,13 +302,13 @@ GEXTEND Gram | IDENT "lapply"; c = lconstr -> TacLApply c (* Derived basic tactics *) - | IDENT "induction"; h = quantified_hypothesis -> TacOldInduction h - | IDENT "newinduction"; c = induction_arg; el = OPT eliminator; + | IDENT "oldinduction"; h = quantified_hypothesis -> TacOldInduction h + | IDENT "induction"; c = induction_arg; el = OPT eliminator; ids = with_names -> TacNewInduction (c,el,ids) | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis; h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) - | IDENT "destruct"; h = quantified_hypothesis -> TacOldDestruct h - | IDENT "newdestruct"; c = induction_arg; el = OPT eliminator; + | IDENT "olddestruct"; h = quantified_hypothesis -> TacOldDestruct h + | IDENT "destruct"; c = induction_arg; el = OPT eliminator; ids = with_names -> TacNewDestruct (c,el,ids) | IDENT "decompose"; IDENT "record" ; c = lconstr -> TacDecomposeAnd c | IDENT "decompose"; IDENT "sum"; c = lconstr -> TacDecomposeOr c |