suite de la reparation du bug 1239: apres les inds, les records et vars de types

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

1 files changed, 14 insertions, 9 deletions

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 2793012e9..46b98dba5 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -392,6 +392,13 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
 	
 (*s Pretty-printing of inductive types declaration. *)
 
+let pp_equiv param_list = function 
+  | None -> mt ()
+  | Some ip_equiv -> 
+      str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv)
+
+let pp_comment s = str "(* " ++ s ++ str " *)"
+
 let pp_one_ind prefix ip ip_equiv pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
@@ -403,16 +410,11 @@ let pp_one_ind prefix ip ip_equiv pl cv =
 			(fun () -> spc () ++ str "* ") (pp_type true pl) l))
   in
   pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++
-  (match ip_equiv with 
-     | None -> mt ()
-     | Some ip_e -> str " = " ++ pp_global (IndRef ip_e)) ++
-  str " =" ++
+  pp_equiv pl ip_equiv ++ str " =" ++
   if Array.length cv = 0 then str " unit (* empty inductive *)" 
   else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
 			(Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
 
-let pp_comment s = str "(* " ++ s ++ str " *)"
-
 let pp_logical_ind packet = 
   pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ 
   fnl () ++ pp_comment (str "with constructors : " ++ 
@@ -426,10 +428,11 @@ let pp_singleton kn packet =
 	 pp_comment (str "singleton inductive, whose constructor was " ++ 
 		     pr_id packet.ip_consnames.(0)))
 
-let pp_record kn projs packet = 
+let pp_record kn projs ip_equiv packet = 
   let l = List.combine projs packet.ip_types.(0) in 
   let pl = rename_tvars keywords packet.ip_vars in 
-  str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
+  str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ 
+  pp_equiv pl ip_equiv ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
 	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) 
   ++ str " }"
@@ -475,7 +478,9 @@ let pp_mind kn i =
   match i.ind_info with 
     | Singleton -> pp_singleton kn i.ind_packets.(0)
     | Coinductive -> pp_ind true kn i
-    | Record projs -> pp_record kn projs i.ind_packets.(0)
+    | Record projs -> 
+	let ip_equiv = option_map (fun kn -> (kn,0)) i.ind_equiv in 
+	pp_record kn projs ip_equiv i.ind_packets.(0)
     | Standard -> pp_ind false kn i
 
 let pp_decl mpl =