reparation bug 1239

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

4 files changed, 34 insertions, 11 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f725c2259..09f03f328 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -310,6 +310,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
   with Not_found -> 
     internal_call := KNset.add kn !internal_call;
     let mib = Environ.lookup_mind kn env in 
+    (* First, if this inductive is aliased via a Module, *)
+    (* we process the original inductive. *)
+    option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in 
@@ -332,7 +335,11 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ip_types = t }) 
 	mib.mind_packets 
     in 
-    add_ind kn {ind_info = Standard; ind_nparams = npar; ind_packets = packets};
+    add_ind kn 
+      {ind_info = Standard; 
+       ind_nparams = npar; 
+       ind_packets = packets; 
+       ind_equiv = mib.mind_equiv };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
       let p = packets.(i) in 
@@ -413,7 +420,11 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	Record field_glob
       with (I info) -> info
     in
-    let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
+    let i = {ind_info = ind_info; 
+	     ind_nparams = npar; 
+	     ind_packets = packets; 
+	     ind_equiv = mib.mind_equiv}
+    in
     add_ind kn i; 
     internal_call := KNset.remove kn !internal_call;
     i
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 8e65a3cd1..2a609f139 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -79,7 +79,9 @@ type ml_ind_packet = {
 type ml_ind = {
   ind_info : inductive_info;
   ind_nparams : int; 	       
-  ind_packets : ml_ind_packet array }
+  ind_packets : ml_ind_packet array;
+  ind_equiv : kernel_name option
+}
 
 (*s ML terms. *)
 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 5c4d48569..eb5c27450 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -195,7 +195,10 @@ let ind_iter_references do_term do_cons do_type kn ind =
   let type_iter = type_iter_references do_type in
   let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
   let packet_iter ip p = 
-    do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
+    do_type (IndRef ip); 
+    if lang () = Ocaml then 
+      option_iter (fun kne -> do_type (IndRef (kne,snd ip))) ind.ind_equiv; 
+    Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
   in
   if lang () = Ocaml then record_iter_references do_term ind.ind_info; 
   Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 18629bcec..2793012e9 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -392,7 +392,7 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
 	
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_one_ind prefix ip pl cv =
+let pp_one_ind prefix ip ip_equiv pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
     hov 2 (str "  | " ++ pp_global r ++
@@ -402,7 +402,11 @@ let pp_one_ind prefix ip pl cv =
 		      prlist_with_sep 
 			(fun () -> spc () ++ str "* ") (pp_type true pl) l))
   in
-  pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ 
+  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 " =" ++
   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))
@@ -434,17 +438,20 @@ let pp_coind ip pl =
   let r = IndRef ip in 
   let pl = rename_tvars keywords pl in
   pp_parameters pl ++ pp_global r ++ str " = " ++ 
-  pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t"
+  pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" ++ 
+  fnl() ++ str "and "
 
 let pp_ind co kn ind =
+  let prefix = if co then "__" else "" in 
   let some = ref false in 
   let init= ref (str "type ") in 
   let rec pp i =  
     if i >= Array.length ind.ind_packets then mt () 
     else 
       let ip = (kn,i) in 
+      let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in 
       let p = ind.ind_packets.(i) in 
-      if is_custom (IndRef (kn,i)) then pp (i+1)
+      if is_custom (IndRef ip) then pp (i+1)
       else begin 
 	some := true; 
 	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
@@ -453,8 +460,8 @@ let pp_ind co kn ind =
 	  begin 
 	    init := (fnl () ++ str "and "); 
 	    s ++
-	    (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ())
-	    ++ pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
+	    (if co then pp_coind ip p.ip_vars else mt ())
+	    ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++
 	    pp (i+1)
 	  end
       end
@@ -574,7 +581,7 @@ let rec pp_structure_elem mpl = function
   | (l,SEmodule m) ->
       hov 1 
 	(str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ 
-	 (* if you want signatures everywhere: *)
+	 (*i if you want signatures everywhere: i*)
 	 (*i str " :" ++ fnl () ++ i*)
 	 (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*)
 	 str " = " ++