Merge branch 'master'.

5 files changed, 43 insertions, 69 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9446cf667..de97ba97c 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -308,15 +308,16 @@ end
 
 module DupMap = Map.Make(DupOrd)
 
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
   let index = ref 0 and dups = ref DupMap.empty in
   register_cleanup (fun () -> index := 0; dups := DupMap.empty);
   let add mp l =
      incr index;
      let ren = "Coq__" ^ string_of_int !index in
      dups := DupMap.add (mp,l) ren !dups
-  and check mp l = DupMap.find (mp, l) !dups
-  in (add,check)
+  and get mp l =
+    try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+  in (add,get)
 
 type reset_kind = AllButExternal | Everything
 
@@ -510,10 +511,11 @@ let pp_duplicate k' prefix mp rls olab =
       (* Here rls=s::rls', we search the label for s inside mp *)
       List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
   in
-  try dottify (check_duplicate prefix lbl :: rls')
-  with Not_found ->
-    assert (get_phase () == Pre); (* otherwise it's too late *)
-    add_duplicate prefix lbl; dottify rls
+  match get_duplicate prefix lbl with
+  | Some ren -> dottify (ren :: rls')
+  | None ->
+     assert (get_phase () == Pre); (* otherwise it's too late *)
+     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
   | [] -> assert false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 2f5601964..b8e95afb3 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path
 val push_visible : module_path -> module_path list -> unit
 val pop_visible : unit -> unit
 
-val check_duplicate : module_path -> Label.t -> string
+val get_duplicate : module_path -> Label.t -> string option
 
 type reset_kind = AllButExternal | Everything
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 52f22ee60..e019bb3c2 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -507,8 +507,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
   in
   (* First, a dry run, for computing objects to rename or duplicate *)
   set_phase Pre;
-  let devnull = formatter true None in
-  pp_with devnull (d.pp_struct struc);
+  ignore (d.pp_struct struc);
   let opened = opened_libraries () in
   (* Print the implementation *)
   let cout = if dry then None else Option.map open_out fn in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 8744eacd3..92ece7ccf 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -267,7 +267,7 @@ let rec extract_type env db j c args =
     | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-	let typ,_ = Typeops.type_of_constant env c in
+        let typ = Typeops.type_of_constant_in env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc2..d89bf95ee 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -555,24 +555,6 @@ let pp_decl = function
     | Dfix (rv,defs,typs) ->
 	pp_Dfix (rv,defs,typs)
 
-let pp_alias_decl ren = function
-  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Dtype (r, l, _) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Dterm (r, a, t) ->
-      let name = pp_global Term r in
-      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
-  | Dfix (rv, _, _) ->
-      prvecti (fun i r -> if is_inline_custom r then mt () else
-		 let name = pp_global Term r in
-		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
-		 fnl ())
-	rv
-
 let pp_spec = function
   | Sval (r,_) when is_inline_custom r -> mt ()
   | Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,42 +579,32 @@ let pp_spec = function
       in
       hov 2 (str "type " ++ ids ++ name ++ def)
 
-let pp_alias_spec ren = function
-  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Stype (r,l,_) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Sval _ -> assert false
-
 let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
   | (l,Spec s) ->
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_spec s
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s
-       with Not_found -> pp_spec s)
+         str ("include module type of struct include "^ren^" end"))
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
-      let def' = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
-       with Not_found -> Pp.mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren ->
+         fnl () ++
+         hov 1 (str ("module "^ren^" :") ++ spc () ++
+                str "module type of struct include " ++ name ++ str " end"))
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> Pp.mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_type params = function
   | MTident kn ->
@@ -653,8 +625,10 @@ and pp_module_type params = function
       let l = List.rev l in
       pop_visible ();
       str "sig" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
-	fnl () ++ str "end"
+      (if List.is_empty l then mt ()
+       else
+         v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+      ++ str "end"
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
       let ids = pp_parameters (rename_tvars keywords vl) in
       let mp_mt = msid_of_mt mt in
@@ -681,12 +655,11 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) ->
-       (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_decl d
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
-	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d
-	with Not_found -> pp_decl d)
+	 fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
@@ -699,18 +672,16 @@ let rec pp_structure_elem = function
       hov 1
 	(str "module " ++ name ++ typ ++ str " =" ++
 	 (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+       | None -> mt ())
   | (l,SEmodtype m) ->
       let def = pp_module_type [] m in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-         fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_expr params = function
   | MEident mp -> pp_modname mp
@@ -732,8 +703,10 @@ and pp_module_expr params = function
       let l = List.rev l in
       pop_visible ();
       str "struct" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
-      fnl () ++ str "end"
+      (if List.is_empty l then mt ()
+       else
+         v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+      ++ str "end"
 
 let rec prlist_sep_nonempty sep f = function
   | [] -> mt ()