diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 7 insertions, 4 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index a64ebb826..b90924f81 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -21,7 +21,7 @@ open Util (* Tactics grammar rules *) GEXTEND Gram - GLOBAL: tactic_expr input_fun; + GLOBAL: tactic_atom tactic_atom0 tactic_expr input_fun; input_fun: [ [ l = identarg -> l | "()" -> <:ast< (VOID) >> ] ] @@ -144,7 +144,8 @@ GEXTEND Gram | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> | st = simple_tactic -> st - | id = lqualid; la = LIST1 tactic_atom0 -> <:ast< (APP $id ($LIST $la)) >> + | id = lqualid; la = LIST1 tactic_atom0 -> + <:ast< (APP $id ($LIST $la)) >> | id = lqualid -> id | ta = tactic_atom0 -> ta ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0c2a61896..a864227a7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,7 +51,7 @@ END (* Gallina declarations *) GEXTEND Gram - GLOBAL: gallina gallina_ext thm_tok theorem_body; + GLOBAL: gallina gallina_ext reduce thm_tok theorem_body; theorem_body_line: [ [ n = numarg; ":"; tac = tacarg; "." -> @@ -105,7 +105,7 @@ GEXTEND Gram ; reduce: [ [ IDENT "Eval"; r = Tactic.red_tactic; "in" -> - [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ] + [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ] | -> [] ] ] ; binders_list: diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ffa82f034..c45c8227d 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -371,6 +371,7 @@ module Vernac_ = let constrarg = gec "constrarg" let ne_constrarg_list = gec_list "ne_constrarg_list" let tacarg = gec "tacarg" + let reduce = gec_list "reduce" let sortarg = gec "sortarg" let theorem_body = gec "theorem_body" let thm_tok = gec "thm_tok" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3b55171b7..781c65162 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -181,6 +181,7 @@ module Vernac_ : val constrarg : Coqast.t Gram.Entry.e val ne_constrarg_list : Coqast.t list Gram.Entry.e val tacarg : Coqast.t Gram.Entry.e + val reduce : Coqast.t list Gram.Entry.e val sortarg : Coqast.t Gram.Entry.e val theorem_body : Coqast.t Gram.Entry.e val thm_tok : Coqast.t Gram.Entry.e |