From 1d3a24bec12a802be171135ddfb805dc4d0cdcee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Apr 2001 21:20:11 +0000
Subject: Uniformisation des 'Save def_tok id'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1564 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_proofs.ml4 | 6 ++----
 parsing/g_vernac.ml4 | 2 +-
 parsing/pcoq.ml4     | 1 +
 parsing/pcoq.mli     | 1 +
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'parsing')

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
-- 
cgit v1.2.3