Remove (useless) aliases from the API.

1 files changed, 13 insertions, 13 deletions

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 83abaf508..16feaf4d6 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -13,7 +13,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Nameops
+open ModPath
 open Globnames
 open Table
 open Miniml
@@ -29,7 +29,7 @@ let pp_tvar id = str ("'" ^ Id.to_string id)
 let pp_abst = function
   | [] -> mt ()
   | l  ->
-      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
+      str "fun " ++ prlist_with_sep (fun () -> str " ") Id.print l ++
       str " ->" ++ spc ()
 
 let pp_parameters l =
@@ -183,7 +183,7 @@ let rec pp_expr par env args =
         (* Try to survive to the occurrence of a Dummy rel.
            TODO: we should get rid of this hack (cf. #592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
-        apply (pr_id id)
+        apply (Id.print id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
@@ -195,7 +195,7 @@ let rec pp_expr par env args =
 	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = pr_id (List.hd i)
+	let pp_id = Id.print (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
@@ -331,10 +331,10 @@ and pp_cons_pat r ppl =
 
 and pp_gen_pat ids env = function
   | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
-  | Pusual r -> pp_cons_pat r (List.map pr_id ids)
+  | Pusual r -> pp_cons_pat r (List.map Id.print ids)
   | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l
   | Pwild -> str "_"
-  | Prel n -> pr_id (get_db_name n env)
+  | Prel n -> Id.print (get_db_name n env)
 
 and pp_ifthenelse env expr pv = match pv with
   | [|([],tru,the);([],fal,els)|] when
@@ -373,7 +373,7 @@ and pp_function env t =
 	  v 0 (pp_pat env' pv)
 	else
           pr_binding (List.rev bl) ++
-          str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+          str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++
 	  v 0 (pp_pat env' pv)
     | _ ->
           pr_binding (List.rev bl) ++
@@ -388,10 +388,10 @@ and pp_fix par env i (ids,bl) args =
     (v 0 (str "let rec " ++
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
-	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
+	    (fun (fi,ti) -> Id.print fi ++ pp_function env ti)
 	    (Array.map2 (fun id b -> (id,b)) ids bl) ++
 	  fnl () ++
-	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+	  hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
 
 (* Ad-hoc double-newline in v boxes, with enough negative whitespace
    to avoid indenting the intermediate blank line *)
@@ -432,7 +432,7 @@ let pp_Dfix (rv,c,t) =
 let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
   | Equiv kn, i ->
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i))
+      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
@@ -452,10 +452,10 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
 let pp_logical_ind packet =
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+  pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   fnl () ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc pr_id packet.ip_consnames) ++
+	      prvect_with_sep spc Id.print packet.ip_consnames) ++
   fnl ()
 
 let pp_singleton kn packet =
@@ -464,7 +464,7 @@ let pp_singleton kn packet =
   hov 2 (str "type " ++ pp_parameters l ++ name ++ 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)))
+		     Id.print packet.ip_consnames.(0)))
 
 let pp_record kn fields ip_equiv packet =
   let ind = IndRef (kn,0) in