diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_proofs.ml4 | 6 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
4 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 6903293bbb..2ce4211fc0 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -50,10 +50,8 @@ GEXTEND Gram | IDENT "Save" -> <:ast< (SaveNamed) >> | IDENT "Defined" -> <:ast< (DefinedNamed) >> | IDENT "Defined"; id = identarg -> <:ast< (DefinedAnonymous $id) >> - | IDENT "Save"; IDENT "Remark"; id = identarg -> - <:ast< (SaveAnonymousRmk $id) >> - | IDENT "Save"; IDENT "Theorem"; id = identarg -> - <:ast< (SaveAnonymousThm $id) >> + | IDENT "Save"; tok = thm_tok; id = identarg -> + <:ast< (SaveAnonymous $tok $id) >> | IDENT "Save"; id = identarg -> <:ast< (SaveAnonymous $id) >> | IDENT "Suspend" -> <:ast< (SUSPEND) >> | IDENT "Resume" -> <:ast< (RESUME) >> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7ed3f645b1..76ffec9a44 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,7 +51,7 @@ END (* Gallina declarations *) GEXTEND Gram - GLOBAL: gallina gallina_ext; + GLOBAL: gallina gallina_ext thm_tok; theorem_body_line: [ [ n = numarg; ":"; tac = tacarg; "." -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 833f8a505e..a5af0845b6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -366,6 +366,7 @@ module Vernac_ = let tacarg = gec "tacarg" let sortarg = gec "sortarg" let theorem_body = gec "theorem_body" + let thm_tok = gec "thm_tok" let gallina = gec "gallina" let gallina_ext = gec "gallina_ext" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7044801fa9..20bf35dea4 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -178,6 +178,7 @@ module Vernac_ : val tacarg : Coqast.t 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 val gallina : Coqast.t Gram.Entry.e val gallina_ext : Coqast.t Gram.Entry.e |