diff options
| author | delahaye | 2001-04-19 04:58:05 +0000 |
|---|---|---|
| committer | delahaye | 2001-04-19 04:58:05 +0000 |
| commit | 88ea1c5d177c68f08fcf26f9f64bdea730aaf03b (patch) | |
| tree | d06ff080078aa849017e4158dd2c8213c887d9c7 | |
| parent | 167542532bea243ef0146480368654613bda631c (diff) | |
Essais dans Ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1606 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 205026ed68..293fe9109b 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -51,7 +51,8 @@ GEXTEND Gram [ [ id = Constr.ident -> id ] ] ; qualidarg: - [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> ] ] + [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> + | "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ] ; qualidconstarg: [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST l)) >> ] ] @@ -227,7 +228,7 @@ GEXTEND Gram | "()" -> <:ast< (VOID) >> ] ] ; let_clause: - [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >> + [ [ id = identarg; "="; te=tactic_atom -> <:ast< (LETCLAUSE $id $te) >> | id = identarg; ":"; c = constrarg; ":="; "Proof" -> (match c with | Coqast.Node(_,"COMMAND",[csr]) -> |