From e6d2309432e62b38d689777c28ef84ce495c8b27 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 16 Dec 2001 09:03:08 +0000
Subject: Ajout syntaxe 'Canonical Structure' en remplacement de @Definition +
 suppression des @Coercion, @Local et @Local Coercion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2299 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4      | 23 +++++++++++++++++++----
 toplevel/vernacentries.ml |  9 +++++++++
 2 files changed, 28 insertions(+), 4 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index accb5d9586..caae9a1e40 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -77,10 +77,6 @@ GEXTEND Gram
   def_tok:
     [ [ "Definition" -> <:ast< "DEFINITION" >>
       | IDENT "Local" -> <:ast< "LOCAL" >> 
-      | "@"; "Definition"  -> <:ast< "OBJECT" >>
-      | "@"; IDENT "Local"  -> <:ast< "LOBJECT" >>
-      | "@"; IDENT "Coercion"  -> <:ast< "OBJCOERCION" >>
-      | "@"; IDENT "Local"; IDENT "Coercion"  -> <:ast< "LOBJCOERCION" >>
       | IDENT "SubClass"  -> <:ast< "SUBCLASS" >>
       | IDENT "Local"; IDENT "SubClass"  -> <:ast< "LSUBCLASS" >> ] ]  
   ;
@@ -324,6 +320,7 @@ GEXTEND Gram
           <:ast< (CONSTR (CAST $c1 $c2)) >>
       | c = Constr.constr -> <:ast< (CONSTR $c) >>
   ] ];
+
   gallina_ext:
     [ [ 
 (* Sections *)
@@ -338,6 +335,24 @@ GEXTEND Gram
       | IDENT "Opaque"; l = ne_qualidarg_list -> 
 	  <:ast< (OPAQUE ($LIST $l)) >>
 
+(* Canonical structure *)
+      | IDENT "Canonical"; IDENT "Structure"; qid = qualidarg ->
+          <:ast< (CANONICAL $qid) >>
+      | IDENT "Canonical"; IDENT "Structure"; qid = qualidarg; ":"; 
+	t = Constr.constr; ":="; c = Constr.constr ->
+          let s = Ast.coerce_to_var qid in
+          <:ast< (DEFINITION "OBJECT" $s (CONSTR $c) (CONSTR $t)) >>
+      | IDENT "Canonical"; IDENT "Structure"; qid = qualidarg; ":="; 
+	c = Constr.constr; ":"; t = Constr.constr ->
+          let s = Ast.coerce_to_var qid in
+          <:ast< (DEFINITION "OBJECT" $s (CONSTR $c) (CONSTR $t)) >>
+      | IDENT "Canonical"; IDENT "Structure"; qid = qualidarg; ":="; 
+	c = Constr.constr ->
+          let s = Ast.coerce_to_var qid in
+          <:ast< (DEFINITION "OBJECT" $s (CONSTR $c)) >>
+      (* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
+         (they were unused and undocumented *)
+
 (* Coercions *)
       | IDENT "Coercion"; qid = qualidarg; ":="; c = def_body ->
           let s = Ast.coerce_to_var qid in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d5366f8c60..b603b28e33 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -915,6 +915,15 @@ let _ =
              if objdef then Recordobj.objdef_declare ref
        | _ -> bad_vernac_args "DEFINITION")
 
+let _ =
+  add "CANONICAL"
+    (function
+       | [VARG_QUALID qid] -> 
+	   fun () ->
+	     let ref = Nametab.global dummy_loc qid in
+	     Recordobj.objdef_declare ref
+       | _ -> bad_vernac_args "CANONICAL")
+
 let _ =
   add "VARIABLE"
     (function 
-- 
cgit v1.2.3