diff options
| author | herbelin | 2003-05-21 13:13:06 +0000 |
|---|---|---|
| committer | herbelin | 2003-05-21 13:13:06 +0000 |
| commit | 6b68976978fc8b4e9589a35858bd5592347be635 (patch) | |
| tree | 63451122a67cd8db0016efb02f0a2330828c49c7 /parsing | |
| parent | 1e160525650bb03c286d78f061f73dcd865b0937 (diff) | |
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour les metavariables de patterns; réparation local défs récursive dans ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 7 | ||||
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 8 |
2 files changed, 6 insertions, 9 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 5c74f4ef62..fb3850c900 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -96,8 +96,7 @@ GEXTEND Gram | pc = Constr.constr_pattern -> Term pc ] ] ; match_hyps: - [ [ id = identref; ":"; mp = match_pattern -> Hyp (id, mp) - | IDENT "_"; ":"; mp = match_pattern -> NoHypId mp ] ] + [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] ; match_context_rule: [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; mp = match_pattern; "]"; @@ -146,8 +145,8 @@ GEXTEND Gram | IDENT "Rec"; rc = rec_clause -> warning "'Rec f ...' is obsolete; use 'Rec f ... In f' instead"; TacLetRecIn ([rc],TacArg (Reference (Libnames.Ident (fst rc)))) - | IDENT "Rec"; rcl = LIST1 rec_clause SEP "And"; IDENT "In"; - body = tactic_expr -> TacLetRecIn (rcl,body) + | IDENT "Rec"; rc = rec_clause; rcl = LIST0 rec_clause SEP "And"; + [IDENT "In" | "in"]; body = tactic_expr -> TacLetRecIn (rc::rcl,body) | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In"; u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) (* Let cas LetCut est subsumé par "Assert id := c" tandis que le cas diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index b364bb8747..834e978e48 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -89,7 +89,7 @@ GEXTEND Gram | "1" RIGHTA [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr -> TacFun (it,body) - | IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; + | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in"; body = tactic_expr -> TacLetRecIn (rcl,body) | "let"; llc = LIST1 let_clause SEP "with"; "in"; u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u) @@ -136,7 +136,6 @@ GEXTEND Gram tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) | r = reference -> Reference r - | "?"; n = natural -> ConstrMayEval (ConstrTerm (CPatVar (loc,(false,Pattern.patvar_of_int n)))) | "()" -> TacVoid ] ] ; input_fun: @@ -154,7 +153,7 @@ GEXTEND Gram LETTOPCLAUSE (id, c) ] ] ; rec_clause: - [ [ name = identref; it = LIST1 input_fun; "=>"; body = tactic_expr -> + [ [ name = identref; it = LIST1 input_fun; ":="; body = tactic_expr -> (name,(it,body)) ] ] ; match_pattern: @@ -164,8 +163,7 @@ GEXTEND Gram | pc = Constr.constr_pattern -> Term pc ] ] ; match_hyps: - [ [ id = identref; ":"; mp = match_pattern -> Hyp (id, mp) - | IDENT "_"; ":"; mp = match_pattern -> NoHypId mp ] ] + [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] ; match_context_rule: [ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]"; |