Imported Upstream version 8.5~beta1+dfsg

1 files changed, 174 insertions, 117 deletions

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 1462d3e7..9fdb0205 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,17 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (*i*)
-open Pp
 open Util
 open Names
 open Libnames
-open Nametab
+open Globnames
 open Table
 open Miniml
 (*i*)
@@ -23,14 +22,14 @@ exception Impossible
 
 (*S Names operations. *)
 
-let anonymous_name = id_of_string "x"
-let dummy_name = id_of_string "_"
+let anonymous_name = Id.of_string "x"
+let dummy_name = Id.of_string "_"
 
 let anonymous = Id anonymous_name
 
 let id_of_name = function
   | Anonymous -> anonymous_name
-  | Name id when id = dummy_name -> anonymous_name
+  | Name id when Id.equal id dummy_name -> anonymous_name
   | Name id -> id
 
 let id_of_mlid = function
@@ -54,6 +53,22 @@ let new_meta _ =
   incr meta_count;
   Tmeta {id = !meta_count; contents = None}
 
+let rec eq_ml_type t1 t2 = match t1, t2 with
+| Tarr (tl1, tr1), Tarr (tl2, tr2) ->
+  eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2
+| Tglob (gr1, t1), Tglob (gr2, t2) ->
+  eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2
+| Tvar i1, Tvar i2 -> Int.equal i1 i2
+| Tvar' i1, Tvar' i2 -> Int.equal i1 i2
+| Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2
+| Tdummy k1, Tdummy k2 -> k1 == k2
+| Tunknown, Tunknown -> true
+| Taxiom, Taxiom -> true
+| _ -> false
+
+and eq_ml_meta m1 m2 =
+ Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents
+
 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
 
 let type_subst_list l t =
@@ -86,7 +101,7 @@ let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
 
 let rec type_occurs alpha t =
   match t with
-  | Tmeta {id=beta; contents=None} -> alpha = beta
+  | Tmeta {id=beta; contents=None} -> Int.equal alpha beta
   | Tmeta {contents=Some u} -> type_occurs alpha u
   | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
   | Tglob (r,l) -> List.exists (type_occurs alpha) l
@@ -95,7 +110,7 @@ let rec type_occurs alpha t =
 (*s Most General Unificator *)
 
 let rec mgu = function
-  | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+  | Tmeta m, Tmeta m' when Int.equal m.id m'.id -> ()
   | Tmeta m, t | t, Tmeta m ->
     (match m.contents with
       | Some u -> mgu (u, t)
@@ -103,21 +118,24 @@ let rec mgu = function
       | None -> m.contents <- Some t)
   | Tarr(a, b), Tarr(a', b') ->
       mgu (a, a'); mgu (b, b')
-  | Tglob (r,l), Tglob (r',l') when r = r' ->
+  | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
        List.iter mgu (List.combine l l')
-  | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
+  | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
-  | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
+  | Tvar i, Tvar j when Int.equal i j -> ()
+  | Tvar' i, Tvar' j when  Int.equal i j -> ()
+  | Tunknown, Tunknown -> ()
+  | Taxiom, Taxiom -> ()
   | _ -> raise Impossible
 
 let needs_magic p = try mgu p; false with Impossible -> true
 
-let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
+let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
 
-let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
 
 let generalizable a =
-  lang () <> Ocaml ||
+  lang () != Ocaml ||
     match a with
       | MLapp _ -> false
       | _ -> true (* TODO, this is just an approximation for the moment *)
@@ -148,7 +166,7 @@ module Mlenv = struct
   (* [find_free] finds the free meta in a type. *)
 
   let rec find_free set = function
-    | Tmeta m when m.contents = None -> Metaset.add m set
+    | Tmeta m when Option.is_empty m.contents -> Metaset.add m set
     | Tmeta {contents = Some t} -> find_free set t
     | Tarr (a,b) -> find_free (find_free set a) b
     | Tglob (_,l) -> List.fold_left find_free set l
@@ -172,12 +190,12 @@ module Mlenv = struct
 
   let generalization mle t =
     let c = ref 0 in
-    let map = ref (Intmap.empty : int Intmap.t) in
-    let add_new i = incr c; map := Intmap.add i !c !map; !c in
+    let map = ref (Int.Map.empty : int Int.Map.t) in
+    let add_new i = incr c; map := Int.Map.add i !c !map; !c in
     let rec meta2var t = match t with
       | Tmeta {contents=Some u} -> meta2var u
       | Tmeta ({id=i} as m) ->
-	  (try Tvar (Intmap.find i !map)
+	  (try Tvar (Int.Map.find i !map)
 	   with Not_found ->
 	     if Metaset.mem m mle.free then t
 	     else Tvar (add_new i))
@@ -225,21 +243,6 @@ let type_maxvar t =
     | _ -> n
   in parse 0 t
 
-(*s What are the type variables occurring in [t]. *)
-
-let intset_union_map_list f l =
-  List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
-
-let intset_union_map_array f a =
-  Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
-
-let rec type_listvar = function
-  | Tmeta {contents = Some t} -> type_listvar t
-  | Tvar i | Tvar' i -> Intset.singleton i
-  | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
-  | Tglob (_,l) -> intset_union_map_list type_listvar l
-  | _ -> Intset.empty
-
 (*s From [a -> b -> c] to [[a;b],c]. *)
 
 let rec type_decomp = function
@@ -283,13 +286,13 @@ let type_simpl = type_expand (fun _ -> None)
 (*s Generating a signature from a ML type. *)
 
 let type_to_sign env t = match type_expand env t with
-  | Tdummy d -> Kill d
+  | Tdummy d when not (conservative_types ()) -> Kill d
   | _ -> Keep
 
 let type_to_signature env t =
   let rec f = function
     | Tmeta {contents = Some t} -> f t
-    | Tarr (Tdummy d, b) -> Kill d :: f b
+    | Tarr (Tdummy d, b) when not (conservative_types ())  -> Kill d :: f b
     | Tarr (_, b) -> Keep :: f b
     | _ -> []
   in f (type_expand env t)
@@ -318,7 +321,7 @@ let rec sign_kind = function
 	| NonLogicalSig -> NonLogicalSig
 	| UnsafeLogicalSig -> UnsafeLogicalSig
 	| SafeLogicalSig | EmptySig ->
-	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
+	    if k == Kother then UnsafeLogicalSig else SafeLogicalSig
 
 (* Removing the final [Keep] in a signature *)
 
@@ -326,17 +329,17 @@ let rec sign_no_final_keeps = function
   | [] -> []
   | k :: s ->
       let s' = k :: sign_no_final_keeps s in
-      if s' = [Keep] then [] else s'
+      match s' with [Keep] -> [] | _ -> s'
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
   let rec expunge s t =
-    if s = [] then t else match t with
+    if List.is_empty s then t else match t with
       | Tmeta {contents = Some t} -> expunge s t
       | Tarr (a,b) ->
 	  let t = expunge (List.tl s) b in
-	  if List.hd s = Keep then Tarr (a, t) else t
+	  if List.hd s == Keep then Tarr (a, t) else t
       | Tglob (r,l) ->
 	  (match env r with
 	     | Some mlt -> expunge s (type_subst_list l mlt)
@@ -344,7 +347,7 @@ let type_expunge_from_sign env s t =
       | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
-  if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then
+  if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
     Tarr (Tdummy Kother, t)
   else t
 
@@ -353,7 +356,55 @@ let type_expunge env t =
 
 (*S Generic functions over ML ast terms. *)
 
-let mlapp f a = if a = [] then f else MLapp (f,a)
+let mlapp f a = if List.is_empty a then f else MLapp (f,a)
+
+(** Equality *)
+
+let eq_ml_ident i1 i2 = match i1, i2 with
+| Dummy, Dummy -> true
+| Id id1, Id id2 -> Id.equal id1 id2
+| Tmp id1, Tmp id2 -> Id.equal id1 id2
+| _ -> false
+
+let rec eq_ml_ast t1 t2 = match t1, t2 with
+| MLrel i1, MLrel i2 ->
+  Int.equal i1 i2
+| MLapp (f1, t1), MLapp (f2, t2) ->
+  eq_ml_ast f1 f2 && List.equal eq_ml_ast t1 t2
+| MLlam (na1, t1), MLlam (na2, t2) ->
+  eq_ml_ident na1 na2 && eq_ml_ast t1 t2
+| MLletin (na1, c1, t1), MLletin (na2, c2, t2) ->
+  eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2
+| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2
+| MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) ->
+  eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2
+| MLtuple t1, MLtuple t2 ->
+  List.equal eq_ml_ast t1 t2
+| MLcase (t1, c1, p1), MLcase (t2, c2, p2) ->
+  eq_ml_type t1 t2 && eq_ml_ast c1 c2 && Array.equal eq_ml_branch p1 p2
+| MLfix (i1, id1, t1), MLfix (i2, id2, t2) ->
+  Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2
+| MLexn e1, MLexn e2 -> String.equal e1 e2
+| MLdummy, MLdummy -> true
+| MLaxiom, MLaxiom -> true
+| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
+| _ -> false
+
+and eq_ml_pattern p1 p2 = match p1, p2 with
+| Pcons (gr1, p1), Pcons (gr2, p2) ->
+  eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2
+| Ptuple p1, Ptuple p2 ->
+  List.equal eq_ml_pattern p1 p2
+| Prel i1, Prel i2 ->
+  Int.equal i1 i2
+| Pwild, Pwild -> true
+| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2
+| _ -> false
+
+and eq_ml_branch (id1, p1, t1) (id2, p2, t2) =
+  List.equal eq_ml_ident id1 id2 &&
+  eq_ml_pattern p1 p2 &&
+  eq_ml_ast t1 t2
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
@@ -428,7 +479,7 @@ let ast_iter f = function
 
 let ast_occurs k t =
   try
-    ast_iter_rel (fun i -> if i = k then raise Found) t; false
+    ast_iter_rel (fun i -> if Int.equal i k then raise Found) t; false
   with Found -> true
 
 (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
@@ -444,7 +495,7 @@ let ast_occurs_itvl k k' t =
 
 let nb_occur_match =
   let rec nb k = function
-    | MLrel i -> if i = k then 1 else 0
+    | MLrel i -> if Int.equal i k then 1 else 0
     | MLcase(_,a,v) ->
         (nb k a) +
 	Array.fold_left
@@ -466,7 +517,7 @@ let ast_lift k t =
   let rec liftrec n = function
     | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
     | a -> ast_map_lift liftrec n a
-  in if k = 0 then t else liftrec 0 t
+  in if Int.equal k 0 then t else liftrec 0 t
 
 let ast_pop t = ast_lift (-1) t
 
@@ -490,7 +541,7 @@ let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
 	let i' = i-n in
-	if i'=1 then ast_lift n e
+	if Int.equal i' 1 then ast_lift n e
 	else if i'<1 then a
 	else MLrel (i-1)
     | a -> ast_map_lift subst n a
@@ -525,17 +576,18 @@ let has_deep_pattern br =
     | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l)
     | Pusual _ | Prel _ | Pwild -> false
   in
-  array_exists (function (_,pat,_) -> deep pat) br
+  Array.exists (function (_,pat,_) -> deep pat) br
 
 let is_regular_match br =
-  if Array.length br = 0 then false (* empty match becomes MLexn *)
+  if Array.is_empty br then false (* empty match becomes MLexn *)
   else
     try
       let get_r (ids,pat,c) =
 	match pat with
 	  | Pusual r -> r
 	  | Pcons (r,l) ->
-	    if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+            let is_rel i = function Prel j -> Int.equal i j | _ -> false in
+	    if not (List.for_all_i is_rel 1 (List.rev l))
 	    then raise Impossible;
 	    r
 	  | _ -> raise Impossible
@@ -544,7 +596,11 @@ let is_regular_match br =
 	| ConstructRef (ind,_) -> ind
 	| _ -> raise Impossible
       in
-      array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+      let is_ref i tr = match get_r tr with
+      | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+      | _ -> false
+      in
+      Array.for_all_i is_ref 0 br
     with Impossible -> false
 
 (*S Operations concerning lambdas. *)
@@ -562,7 +618,7 @@ let collect_lams =
 
 let collect_n_lams =
   let rec collect acc n t =
-    if n = 0 then acc,t
+    if Int.equal n 0 then acc,t
     else match t with
       | MLlam(id,t) -> collect (id::acc) (n-1) t
       | _ -> assert false
@@ -571,7 +627,7 @@ let collect_n_lams =
 (*s [remove_n_lams] just removes some [MLlam]. *)
 
 let rec remove_n_lams n t =
-  if n = 0 then t
+  if Int.equal n 0 then t
   else match t with
       | MLlam(_,t) -> remove_n_lams (n-1) t
       | _ -> assert false
@@ -609,7 +665,7 @@ let rec anonym_or_dummy_lams a = function
 (*s The following function creates [MLrel n;...;MLrel 1] *)
 
 let rec eta_args n =
-  if n = 0 then [] else (MLrel n)::(eta_args (pred n))
+  if Int.equal n 0 then [] else (MLrel n)::(eta_args (pred n))
 
 (*s Same, but filtered by a signature. *)
 
@@ -621,25 +677,26 @@ let rec eta_args_sign n = function
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
 let rec test_eta_args_lift k n = function
-  | [] -> n=0
-  | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
+  | [] -> Int.equal n 0
+  | MLrel m :: q -> Int.equal (k+n) m && (test_eta_args_lift k (pred n) q)
+  | _ -> false
 
 (*s Computes an eta-reduction. *)
 
 let eta_red e =
   let ids,t = collect_lams e in
   let n = List.length ids in
-  if n = 0 then e
+  if Int.equal n 0 then e
   else match t with
     | MLapp (f,a) ->
 	let m = List.length a in
 	let ids,body,args =
-	  if m = n then
+	  if Int.equal m n then
 	    [], f, a
 	  else if m < n then
-	    list_skipn m ids, f, a
+	    List.skipn m ids, f, a
 	  else (* m > n *)
-	    let a1,a2 = list_chop (m-n) a in
+	    let a1,a2 = List.chop (m-n) a in
 	    [], MLapp (f,a1), a2
 	in
 	let p = List.length args in
@@ -715,7 +772,7 @@ let branch_as_fun typ (l,p,c) =
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
+    | MLcons _ as cons' when eq_ml_ast cons' (ast_lift n cons) -> MLrel (n+1)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
@@ -739,27 +796,33 @@ let branch_as_cst (l,_,c) =
    When searching for the best factorisation below, we'll try both.
 *)
 
-(* The following structure allows to record which element occurred
+(* The following structure allows recording which element occurred
    at what position, and then finally return the most frequent
    element and its positions. *)
 
 let census_add, census_max, census_clean =
-  let h = Hashtbl.create 13 in
-  let clear () = Hashtbl.clear h in
-  let add e i =
-    let s = try Hashtbl.find h e with Not_found -> Intset.empty in
-    Hashtbl.replace h e (Intset.add i s)
+  let h = ref [] in
+  let clearf () = h := [] in
+  let rec add k v = function
+  | [] -> raise Not_found
+  | (k', s) as p :: l ->
+    if eq_ml_ast k k' then (k', Int.Set.add v s) :: l
+    else p :: add k v l
+  in
+  let addf k i =
+    try h := add k i !h
+    with Not_found -> h := (k, Int.Set.singleton i) :: !h
   in
-  let max e0 =
-    let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
-    Hashtbl.iter
-      (fun e s ->
-	 let n = Intset.cardinal s in
+  let maxf k =
+    let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in
+    List.iter
+      (fun (e, s) ->
+	 let n = Int.Set.cardinal s in
 	 if n > !len then begin len := n; lst := s; elm := e end)
-      h;
+      !h;
     (!elm,!lst)
   in
-  (add,max,clear)
+  (addf,maxf,clearf)
 
 (* [factor_branches] return the longest possible list of branches
    that have the same factorization, either as a function or as a
@@ -771,7 +834,7 @@ let is_opt_pat (_,p,_) = match p with
   | _ -> false
 
 let factor_branches o typ br =
-  if array_exists is_opt_pat br then None (* already optimized *)
+  if Array.exists is_opt_pat br then None (* already optimized *)
   else begin
     census_clean ();
     for i = 0 to Array.length br - 1 do
@@ -782,8 +845,8 @@ let factor_branches o typ br =
     done;
     let br_factor, br_set = census_max MLdummy in
     census_clean ();
-    let n = Intset.cardinal br_set in
-    if n = 0 then None
+    let n = Int.Set.cardinal br_set in
+    if Int.equal n 0 then None
     else if Array.length br >= 2 && n < 2 then None
     else Some (br_factor, br_set)
   end
@@ -794,17 +857,17 @@ let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
   | l,[] -> l
   | i::ids, i'::ids' ->
-      (if i = Dummy then i' else i) :: (merge_ids ids ids')
+      (if i == Dummy then i' else i) :: (merge_ids ids ids')
 
 let is_exn = function MLexn _ -> true | _ -> false
 
-let rec permut_case_fun br acc =
+let permut_case_fun br acc =
   let nb = ref max_int in
   Array.iter (fun (_,_,t) ->
 		let ids, c = collect_lams t in
 		let n = List.length ids in
 		if (n < !nb) && (not (is_exn c)) then nb := n) br;
-  if !nb = max_int || !nb = 0 then ([],br)
+  if Int.equal !nb  max_int || Int.equal !nb 0 then ([],br)
   else begin
     let br = Array.copy br in
     let ids = ref [] in
@@ -837,16 +900,16 @@ let rec iota_red i lift br ((typ,r,a) as cons) =
   if i >= Array.length br then raise Impossible;
   let (ids,p,c) = br.(i) in
   match p with
-    | Pusual r' | Pcons (r',_) when r'<>r -> iota_red (i+1) lift br cons
+    | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons
     | Pusual r' ->
       let c = named_lams (List.rev ids) c in
       let c = ast_lift lift c
       in MLapp (c,a)
-    | Prel 1 when List.length ids = 1 ->
+    | Prel 1 when Int.equal (List.length ids) 1 ->
       let c = MLlam (List.hd ids, c) in
       let c = ast_lift lift c
       in MLapp(c,[MLcons(typ,r,a)])
-    | Pwild when ids = [] -> ast_lift lift c
+    | Pwild when List.is_empty ids -> ast_lift lift c
     | _ -> raise Impossible (* TODO: handle some more cases *)
 
 (* [iota_gen] is an extension of [iota_red] where we allow to
@@ -872,15 +935,11 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
     Unfolding them leads to more natural code (and more dummy removal) *)
 
 let is_program_branch = function
-  | Id id ->
-    let s = string_of_id id in
-    let br = "program_branch_" in
-    let n = String.length br in
-    (try
-       ignore (int_of_string (String.sub s n (String.length s - n)));
-       String.sub s 0 n = br
-     with e when Errors.noncritical e -> false)
   | Tmp _ | Dummy -> false
+  | Id id ->
+    let s = Id.to_string id in
+    try Scanf.sscanf s "program_branch_%d%!" (fun _ -> true)
+    with Scanf.Scan_failure _ | End_of_file -> false
 
 let expand_linear_let o id e =
    o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
@@ -901,7 +960,7 @@ let rec simpl o = function
       if
 	(is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in
-	 (n = 0 || (n=1 && expand_linear_let o id e)))
+	 (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
       then
 	simpl o (ast_subst c e)
       else
@@ -954,14 +1013,14 @@ and simpl_case o typ br e =
     (* Swap the case and the lam if possible *)
     let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
     let n = List.length ids in
-    if n <> 0 then
+    if not (Int.equal n 0) then
       simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
     else
       (* Can we merge several branches as the same constant or function ? *)
-      if lang() = Scheme || is_custom_match br
+      if lang() == Scheme || is_custom_match br
       then MLcase (typ, e, br)
       else match factor_branches o typ br with
-	| Some (f,ints) when Intset.cardinal ints = Array.length br ->
+	| Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
 	  (* If all branches have been factorized, we remove the match *)
 	  simpl o (MLletin (Tmp anonymous_name, e, f))
 	| Some (f,ints) ->
@@ -970,7 +1029,7 @@ and simpl_case o typ br e =
 	    else ([], Pwild, ast_pop f)
 	  in
 	  let brl = Array.to_list br in
-	  let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+	  let brl_opt = List.filteri (fun i _ -> not (Int.Set.mem i ints)) brl in
 	  let brl_opt = brl_opt @ [last_br] in
 	  MLcase (typ, e, Array.of_list brl_opt)
 	| None -> MLcase (typ, e, br)
@@ -996,9 +1055,9 @@ let rec select_via_bl l args = match l,args with
 
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
-  if n = n' then ids,c
-  else if n' = 0 then [],ast_lift (-n) c
+  let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
+  if Int.equal n n' then ids,c
+  else if Int.equal n' 0 then [],ast_lift (-n) c
   else begin
     let v = Array.make n None in
     let rec parse_ids i j = function
@@ -1016,15 +1075,15 @@ let kill_some_lams bl (ids,c) =
 let kill_dummy_lams c =
   let ids,c = collect_lams c in
   let bl = List.map sign_of_id ids in
-  if not (List.mem Keep bl) then raise Impossible;
+  if not (List.memq Keep bl) then raise Impossible;
   let rec fst_kill n = function
     | [] -> raise Impossible
     | Kill _ :: bl -> n
     | Keep :: bl -> fst_kill (n+1) bl
   in
   let skip = max 0 ((fst_kill 0 bl) - 1) in
-  let ids_skip, ids = list_chop skip ids in
-  let _, bl = list_chop skip bl in
+  let ids_skip, ids = List.chop skip ids in
+  let _, bl = List.chop skip bl in
   let c = named_lams ids_skip c in
   let ids',c = kill_some_lams bl (ids,c) in
   ids, named_lams ids' c
@@ -1052,7 +1111,7 @@ let case_expunge s e =
   let m = List.length s in
   let n = nb_lams e in
   let p = if m <= n then collect_n_lams m e
-  else eta_expansion_sign (list_skipn n s) (collect_lams e) in
+  else eta_expansion_sign (List.skipn n s) (collect_lams e) in
   kill_some_lams (List.rev s) p
 
 (*s [term_expunge] takes a function [fun idn ... id1 -> c]
@@ -1061,10 +1120,10 @@ let case_expunge s e =
   if all lambdas are logical dummy and the target language is strict. *)
 
 let term_expunge s (ids,c) =
-  if s = [] then c
+  if List.is_empty s then c
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
-    if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then
+    if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
@@ -1076,7 +1135,7 @@ let kill_dummy_args ids r t =
   let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
   let rec found n = function
-    | MLrel r' when r' = r + n -> true
+    | MLrel r' when Int.equal r' (r + n) -> true
     | MLmagic e -> found n e
     | _ -> false
   in
@@ -1086,7 +1145,7 @@ let kill_dummy_args ids r t =
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
 	let a = select_via_bl bl (a @ (eta_args k)) in
-	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+	named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
     | e when found n e ->
 	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
@@ -1153,7 +1212,7 @@ let normalize a =
   let o = optims () in
   let rec norm a =
     let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
-    if a = a' then a else norm a'
+    if eq_ml_ast a a' then a else norm a'
   in norm a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
@@ -1165,7 +1224,7 @@ let general_optimize_fix f ids n args m c =
     | MLrel j when v.(j-1)>=0 ->
 	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
-  in list_iter_i aux args;
+  in List.iteri aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
   let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
   let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
@@ -1176,7 +1235,7 @@ let optimize_fix a =
   else
     let ids,a' = collect_lams a in
     let n = List.length ids in
-    if n = 0 then a
+    if Int.equal n 0 then a
     else match a' with
       | MLfix(_,[|f|],[|c|]) ->
 	  let new_f = MLapp (MLrel (n+1),eta_args n) in
@@ -1244,7 +1303,7 @@ let rec non_stricts add cand = function
       let cand = if add then 1::cand else cand in
       pop 1 (non_stricts add cand t)
   | MLrel n ->
-      List.filter ((<>) n) cand
+      List.filter (fun m -> not (Int.equal m n)) cand
   | MLapp (t,l)->
       let cand = non_stricts false cand t in
       List.fold_left (non_stricts false) cand l
@@ -1268,7 +1327,7 @@ let rec non_stricts add cand = function
 	   let n = List.length i in
 	   let cand = lift n cand in
 	   let cand = pop n (non_stricts add cand t) in
-	   Sort.merge (<=) cand c) [] v
+	   List.merge Int.compare cand c) [] v
 	(* [merge] may duplicates some indices, but I don't mind. *)
   | MLmagic t ->
       non_stricts add cand t
@@ -1304,7 +1363,7 @@ let is_not_strict t =
    restriction for the moment.
 *)
 
-open Declarations
+open Declareops
 
 let inline_test r t =
   if not (auto_inline ()) then false
@@ -1312,7 +1371,7 @@ let inline_test r t =
     let c = match r with ConstRef c -> c | _ -> assert false in
     let has_body =
       try constant_has_body (Global.lookup_constant c)
-      with e when Errors.noncritical e -> false
+      with Not_found -> false
     in
     has_body &&
       (let t1 = eta_red t in
@@ -1320,10 +1379,8 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  let null = empty_dirpath in
-  match repr_dirpath (dirpath_of_string s) with
-    | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
-    | [] -> assert false
+  let d, id = Libnames.split_dirpath (dirpath_of_string s) in
+  Constant.make2 (MPfile d) (Label.of_id id)
 
 let manual_inline_set =
   List.fold_right (fun x -> Cset_env.add (con_of_string x))
@@ -1355,6 +1412,6 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && not (is_inline_custom r)
   && (to_inline r (* The user DOES want to inline it *)
-     || (lang () <> Haskell && not (is_projection r) &&
+     || (lang () != Haskell && not (is_projection r) &&
          (is_recursor r || manual_inline r || inline_test r t)))