Specific syntax for Instances in Module Type: Declare Instance

NB: the grammar entry is placed in vernac:command on purpose
 even if it should have gone into vernac:gallina_ext. Camlp4
 isn't factorising rules starting by "Declare" in a correct way
 otherwise...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 20 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3baed8992d..4672a732a6 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -50,6 +50,7 @@ let decl_notation = Gram.Entry.create "vernac:decl_notation"
 let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
 let record_field = Gram.Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
+let instance_name = Gram.Entry.create "vernac:instance_name"
 
 let get_command_entry () =
   match Decl_mode.get_current_mode () with
@@ -463,7 +464,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
-  GLOBAL: gallina_ext;
+  GLOBAL: gallina_ext instance_name;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -515,28 +516,13 @@ GEXTEND Gram
       | IDENT "Context"; c = binders_let ->
 	  VernacContext c
 
-      | IDENT "Instance"; ":";
+      | IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> r |
 	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
-	   VernacInstance (not (use_section_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
-
-      | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
-	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
-	 pri = OPT [ "|"; i = natural -> i ] ;
-	 props = [ ":="; "{"; r = record_declaration; "}" -> r |
-	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
-	   let sup =
-	     match sup with
-		 None -> []
-	       | Some l -> l
-	   in
-	   let n =
-	     let (loc, id) = name in
-	       (loc, Name id)
-	   in
-	     VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri)
+	   VernacInstance (false, not (use_non_locality ()),
+			   snd namesup, (fst namesup, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = global -> 
 	  VernacDeclareInstance (not (use_section_locality ()), is)
@@ -572,6 +558,13 @@ GEXTEND Gram
       | "-"; n=INT -> Conv_oracle.Level (- int_of_string n)
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
+  instance_name:
+    [ [ name = identref; sup = OPT binders_let ->
+	  (let (loc,id) = name in (loc, Name id)),
+          (Option.default [] sup)
+      | -> (loc, Anonymous), []  ] ]
+  ;
+
 END
 
 GEXTEND Gram
@@ -580,6 +573,14 @@ GEXTEND Gram
   command:
     [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
+      (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
+      | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
+	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+	 pri = OPT [ "|"; i = natural -> i ] ->
+	   VernacInstance (true, not (use_non_locality ()),
+			   snd namesup, (fst namesup, expl, t),
+			   CRecord (loc, None, []), pri)
+
       (* System directory *)
       | IDENT "Pwd" -> VernacChdir None
       | IDENT "Cd" -> VernacChdir None
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 873558dff9..4b1162dbd1 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -719,9 +719,10 @@ let rec pr_vernac = function
 (* 	  prlist_with_sep (fun () -> str";" ++ spc())  *)
 (* 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *)
 
- | VernacInstance (glob, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
        pr_non_locality (not glob) ++
+       (if abst then str"Declare " else mt ()) ++
        str"Instance" ++ spc () ++
 	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++