diff options
| -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]) -> |