plus d'environment fixe cur_env mais un environment evolutif

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

1 files changed, 7 insertions, 9 deletions

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1d6b40372..311c346d5 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -386,20 +386,18 @@ let pp_one_ind prefix ip pl cv =
 
 let pp_comment s = str "(* " ++ s ++ str " *)"
 
-let pp_logical_ind ip packet = 
-  pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++ fnl () ++
-  pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc pr_global 
-		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
+let pp_logical_ind packet = 
+  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ 
+  fnl () ++ pp_comment (str "with constructors : " ++ 
+			prvect_with_sep spc pr_id packet.ip_consnames)
 
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
   hov 2 (str "type " ++ pp_parameters l ++
 	 P.pp_global !local_mp (IndRef (kn,0)) ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment 
-	   (str "singleton inductive, whose constructor was " ++ 
-	    pr_id packet.ip_consnames.(0)))
+	 pp_comment (str "singleton inductive, whose constructor was " ++ 
+		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn packet = 
   let kn = long_kn kn in 
@@ -428,7 +426,7 @@ let pp_ind co kn ind =
       if is_custom (IndRef (kn,i)) then pp (i+1)
       else begin 
 	some := true; 
-	if p.ip_logical then pp_logical_ind ip p ++ pp (i+1)
+	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
 	else 
 	  let s = !init in 
 	  begin