From 03b5cec9dd20905d0af89aa637a024ebfa0e1ac2 Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 9 Nov 2008 16:22:03 +0000
Subject: Oops... forgot to commit a file related to r11561.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11565 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/ppvernac.ml | 38 ++++++++++++++++++--------------------
 1 file changed, 18 insertions(+), 20 deletions(-)

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 3c8613aad..e16b4e533 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -408,9 +408,7 @@ let make_pr_vernac pr_constr pr_lconstr =
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
 let pr_intarg n = spc () ++ int n in
-let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
-let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
-  ++ sep ++ pr_constrarg c in
+(* let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in *)
 let pr_record_field (x, ntn) = 
   let prx = match x with
     | (oc,AssumExpr (id,t)) ->
@@ -427,7 +425,7 @@ let pr_record_field (x, ntn) =
                     pr_lconstr b)) in
     prx ++ pr_decl_notation pr_constr ntn
 in
-let pr_record_decl c fs = 
+let pr_record_decl b c fs = 
     pr_opt pr_lident c ++ str"{"  ++
     hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
 in
@@ -591,14 +589,14 @@ let rec pr_vernac = function
             fnl() ++
             str (if List.length l = 1 then "   " else " | ") ++
             prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l 
-       | RecordDecl (c,fs) ->   
+       | RecordDecl (b,c,fs) ->   
 	    spc() ++
-	    pr_record_decl c fs in
+	    pr_record_decl b c fs in
       let pr_oneind key ((id,indpar,s,lc),ntn) =
 	hov 0 (
           str key ++ spc() ++
-          pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ str":" ++ 
-	  spc() ++ pr_lconstr_expr s ++ 
+          pr_lident id ++ pr_and_type_binders_arg indpar ++ spc() ++ 
+	    Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++ 
 	  str" :=") ++ pr_constructor_list lc ++ 
 	pr_decl_notation pr_constr ntn in
 
@@ -669,10 +667,10 @@ let rec pr_vernac = function
   (* Gallina extensions *)
   | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) ->
       hov 2
-        (str (if b then "Record" else "Structure") ++
+        (str (if b then "Record" else "Class") ++
          (if oc then str" > " else str" ") ++ pr_lident name ++ 
           pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
-	  pr_lconstr_expr s ++ str" := " ++ pr_record_decl c fs)
+	  Option.cata pr_lconstr_expr (mt()) s ++ str" := " ++ pr_record_decl b c fs)
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
   | VernacRequire (exp,spe,l) -> hov 2
@@ -701,15 +699,15 @@ let rec pr_vernac = function
 	spc() ++ pr_class_rawexpr c2)
 
 
-  | VernacClass (id, par, ar, sup, props) ->
-      hov 1 (
-	str"Class" ++ spc () ++ pr_lident id ++
-(* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *)
-	  pr_and_type_binders_arg par ++
-	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++
-	  spc () ++ str":=" ++ spc () ++
-	  prlist_with_sep (fun () -> str";" ++ spc()) 
-	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
+(*   | VernacClass (id, par, ar, sup, props) -> *)
+(*       hov 1 ( *)
+(* 	str"Class" ++ spc () ++ pr_lident id ++ *)
+(* (\* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *\) *)
+(* 	  pr_and_type_binders_arg par ++ *)
+(* 	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) | None -> mt()) ++ *)
+(* 	  spc () ++ str":=" ++ spc () ++ *)
+(* 	  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) -> 
      hov 1 (
@@ -720,7 +718,7 @@ let rec pr_vernac = function
 	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
 	 pr_constr_expr cl ++ spc () ++
 	 spc () ++ str":=" ++ spc () ++
-	 prlist_with_sep (fun () -> str";" ++ spc()) (pr_instance_def (spc () ++ str":=" ++ spc())) props)
+	 pr_constr_expr props)
 
  | VernacContext l ->
      hov 1 (
-- 
cgit v1.2.3