Applying François Garillot's patch (#2261 in bug tracker) for extended

syntax of "Implicit Type" (that can now be "Implicit Types" and can
now accept several blocks of variables of a given type).

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

2 files changed, 26 insertions, 7 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a0f9dcaefa..008a6ac510 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -120,6 +120,12 @@ let test_plurial_form = function
    "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
   | _ -> ()
 
+let test_plurial_form_types = function
+  | [([_],_)] ->
+      Flags.if_verbose warning
+   "Keywords Implicit Types expect more than one type"
+  | _ -> ()
+
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
@@ -546,8 +552,12 @@ GEXTEND Gram
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
-      | IDENT "Implicit"; ["Type" | IDENT "Types"];
-	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c)
+      | IDENT "Implicit"; "Type"; bl = reserv_list ->
+	   VernacReserve bl
+
+      | IDENT "Implicit"; IDENT "Types"; bl = reserv_list ->
+          test_plurial_form_types bl;
+           VernacReserve bl
 
       | IDENT "Generalizable"; 
 	   gen = [IDENT "All"; IDENT "Variables" -> Some []
@@ -575,6 +585,15 @@ GEXTEND Gram
           (Option.default [] sup)
       | -> (loc, Anonymous), []  ] ]
   ;
+  reserv_list:
+    [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ]
+  ;
+  reserv_tuple:
+    [ [ "("; a = simple_reserv; ")" -> a ] ]
+  ;
+  simple_reserv:
+    [ [ idl = LIST1 identref; ":"; c = lconstr -> (idl,c) ] ]
+  ;
 
 END
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index ff480a5d44..9ebf77adba 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -851,11 +851,11 @@ let rec pr_vernac = function
       hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ 
 	spc() ++ pr_smart_global q ++ spc() ++
 	str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
-  | VernacReserve (idl,c) ->
-      hov 1 (str"Implicit Type" ++
-        str (if List.length idl > 1 then "s " else " ") ++
-        prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++
-        pr_lconstr c)
+  | VernacReserve bl ->
+      let n = List.length (List.flatten (List.map fst bl)) in
+      hov 2 (str"Implicit Type" ++
+        str (if n > 1 then "s " else " ") ++
+        pr_ne_params_list pr_lconstr_expr (List.map (fun sb -> false,sb) bl))
   | VernacGeneralizable (local, g) ->
       hov 1 (pr_locality local ++ str"Generalizable Variable" ++
 		match g with