Moved Intset and Intmap to Int namespace.

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

37 files changed, 276 insertions, 271 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 20e0fff55..89c2179d2 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -60,7 +60,7 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 let ppbigint n = pp (str (Bigint.to_string n));;
 
 let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]"
-let ppintset l = pp (prset int (Intset.elements l))
+let ppintset l = pp (prset int (Int.Set.elements l))
 let ppidset l = pp (prset pr_id (Idset.elements l))
 
 let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]"
diff --git a/lib/int.ml b/lib/int.ml
index 19cdfac0a..86d79fd31 100644
--- a/lib/int.ml
+++ b/lib/int.ml
@@ -13,3 +13,12 @@ external equal : int -> int -> bool = "%eq"
 external compare : int -> int -> int = "caml_int_compare"
 
 let hash i = i land max_int
+
+module Self =
+struct
+  type t = int
+  let compare = compare
+end
+
+module Set = Set.Make(Self)
+module Map = Map.Make(Self)
diff --git a/lib/int.mli b/lib/int.mli
index ae1a32dc8..cde422a84 100644
--- a/lib/int.mli
+++ b/lib/int.mli
@@ -15,3 +15,6 @@ external equal : t -> t -> bool = "%eq"
 external compare : t -> t -> int = "caml_int_compare"
 
 val hash : t -> int
+
+module Set : Set.S with type elt = t
+module Map : Map.S with type key = t
diff --git a/lib/store.ml b/lib/store.ml
index ad6595ade..536e5f280 100644
--- a/lib/store.ml
+++ b/lib/store.ml
@@ -21,7 +21,7 @@ let next =
   incr count;
   n
 
-type t = Obj.t Util.Intmap.t
+type t = Obj.t Int.Map.t
 
 module Field = struct
   type 'a field = {
@@ -34,18 +34,18 @@ end
 
 open Field
 
-let empty = Util.Intmap.empty
+let empty = Int.Map.empty
 
 let field () =
   let fid = next () in
   let set a s =
-    Util.Intmap.add fid (Obj.repr a) s
+    Int.Map.add fid (Obj.repr a) s
   in
   let get s =
-    try Some (Obj.obj (Util.Intmap.find fid s))
+    try Some (Obj.obj (Int.Map.find fid s))
     with _ -> None
   in
   let remove s =
-    Util.Intmap.remove fid s
+    Int.Map.remove fid s
   in
   { set = set ; get = get ; remove = remove }
diff --git a/lib/util.ml b/lib/util.ml
index 8d8c947c7..91497f370 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -119,9 +119,6 @@ let delayed_force f = f ()
 
 type ('a,'b) union = Inl of 'a | Inr of 'b
 
-module Intset = Set.Make(Int)
-module Intmap = Map.Make(Int)
-
 (*s interruption *)
 
 let interrupt = ref false
diff --git a/lib/util.mli b/lib/util.mli
index 6dc6c703d..e6cb7fe9d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -84,10 +84,6 @@ val delayed_force : 'a delayed -> 'a
 
 type ('a, 'b) union = Inl of 'a | Inr of 'b
 
-module Intset : Set.S with type elt = int
-
-module Intmap : Map.S with type key = int
-
 (** {6 ... } *)
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 89e30a8ee..2155171c9 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -65,7 +65,7 @@ module ST=struct
     with
 	Not_found -> ()
 
-  let delete_set st s = Intset.iter (delete st) s
+  let delete_set st s = Int.Set.iter (delete st) s
 
 end
 
@@ -172,11 +172,11 @@ type inductive_status =
 
 type representative=
     {mutable weight:int;
-     mutable lfathers:Intset.t;
-     mutable fathers:Intset.t;
+     mutable lfathers:Int.Set.t;
+     mutable fathers:Int.Set.t;
      mutable inductive_status: inductive_status;
      class_type : Term.types;
-     mutable functions: Intset.t PafMap.t;
+     mutable functions: Int.Set.t PafMap.t;
      mutable constructors: int PacMap.t} (*pac -> term = app(constr,t) *)
 
 type cl = Rep of representative| Eqto of int*equality
@@ -219,16 +219,16 @@ type forest=
 type state =
     {uf: forest;
      sigtable:ST.t;
-     mutable terms: Intset.t;
+     mutable terms: Int.Set.t;
      combine: equality Queue.t;
      marks: (int * pa_mark) Queue.t;
      mutable diseq: disequality list;
      mutable quant: quant_eq list;
-     mutable pa_classes: Intset.t;
+     mutable pa_classes: Int.Set.t;
      q_history: (int array) Identhash.t;
      mutable rew_depth:int;
      mutable changed:bool;
-     by_type: Intset.t Typehash.t;
+     by_type: Int.Set.t Typehash.t;
      mutable gls:Proof_type.goal Tacmach.sigma}
 
 let dummy_node =
@@ -245,13 +245,13 @@ let empty depth gls:state =
       epsilons=[];
       axioms=Constrhash.create init_size;
       syms=Termhash.create init_size};
-  terms=Intset.empty;
+  terms=Int.Set.empty;
   combine=Queue.create ();
   marks=Queue.create ();
   sigtable=ST.empty ();
   diseq=[];
   quant=[];
-  pa_classes=Intset.empty;
+  pa_classes=Int.Set.empty;
   q_history=Identhash.create init_size;
   rew_depth=depth;
   by_type=Constrhash.create init_size;
@@ -292,13 +292,13 @@ let epsilons uf = uf.epsilons
 let add_lfather uf i t=
   let r=get_representative uf i in
     r.weight<-r.weight+1;
-    r.lfathers<-Intset.add t r.lfathers;
-    r.fathers <-Intset.add t r.fathers
+    r.lfathers<-Int.Set.add t r.lfathers;
+    r.fathers <-Int.Set.add t r.fathers
 
 let add_rfather uf i t=
   let r=get_representative uf i in
     r.weight<-r.weight+1;
-    r.fathers <-Intset.add t r.fathers
+    r.fathers <-Int.Set.add t r.fathers
 
 exception Discriminable of int * pa_constructor * int * pa_constructor
 
@@ -317,8 +317,8 @@ let add_pac rep pac t =
 
 let add_paf rep paf t =
   let already =
-    try PafMap.find paf rep.functions with Not_found -> Intset.empty in
-    rep.functions<- PafMap.add paf (Intset.add t already) rep.functions
+    try PafMap.find paf rep.functions with Not_found -> Int.Set.empty in
+    rep.functions<- PafMap.add paf (Int.Set.add t already) rep.functions
 
 let term uf i=uf.map.(i).term
 
@@ -347,8 +347,8 @@ let next uf=
 
 let new_representative typ =
   {weight=0;
-   lfathers=Intset.empty;
-   fathers=Intset.empty;
+   lfathers=Int.Set.empty;
+   fathers=Int.Set.empty;
    inductive_status=Unknown;
    class_type=typ;
    functions=PafMap.empty;
@@ -445,7 +445,7 @@ let rec add_term state t=
 		  let i1=add_term state t1 and i2=add_term state t2 in
 		    add_lfather uf (find uf i1) b;
 		    add_rfather uf (find uf i2) b;
-		    state.terms<-Intset.add b state.terms;
+		    state.terms<-Int.Set.add b state.terms;
 		    {clas= Rep (new_representative typ);
 		     cpath= -1;
 		     vertex= Node(i1,i2);
@@ -468,9 +468,9 @@ let rec add_term state t=
 	    uf.map.(b)<-new_node;
 	    Termhash.add uf.syms t b;
 	    Typehash.replace state.by_type typ
-	      (Intset.add b
+	      (Int.Set.add b
 		 (try Typehash.find state.by_type typ with
-		      Not_found -> Intset.empty));
+		      Not_found -> Int.Set.empty));
 	    b
 
 let add_equality state c s t=
@@ -567,34 +567,34 @@ let union state i1 i2 eq=
   and r2= get_representative state.uf i2 in
     link state.uf i1 i2 eq;
     Constrhash.replace state.by_type r1.class_type
-      (Intset.remove i1
+      (Int.Set.remove i1
 	 (try Constrhash.find state.by_type r1.class_type with
-	      Not_found -> Intset.empty));
-    let f= Intset.union r1.fathers r2.fathers in
-      r2.weight<-Intset.cardinal f;
+	      Not_found -> Int.Set.empty));
+    let f= Int.Set.union r1.fathers r2.fathers in
+      r2.weight<-Int.Set.cardinal f;
       r2.fathers<-f;
-      r2.lfathers<-Intset.union r1.lfathers r2.lfathers;
+      r2.lfathers<-Int.Set.union r1.lfathers r2.lfathers;
       ST.delete_set state.sigtable r1.fathers;
-      state.terms<-Intset.union state.terms r1.fathers;
+      state.terms<-Int.Set.union state.terms r1.fathers;
       PacMap.iter
 	(fun pac b -> Queue.add (b,Cmark pac) state.marks)
 	r1.constructors;
       PafMap.iter
-	(fun paf -> Intset.iter
+	(fun paf -> Int.Set.iter
 	   (fun b -> Queue.add (b,Fmark paf) state.marks))
 	r1.functions;
       match r1.inductive_status,r2.inductive_status with
 	  Unknown,_ -> ()
 	| Partial pac,Unknown ->
 	    r2.inductive_status<-Partial pac;
-	    state.pa_classes<-Intset.remove i1 state.pa_classes;
-	    state.pa_classes<-Intset.add i2 state.pa_classes
+	    state.pa_classes<-Int.Set.remove i1 state.pa_classes;
+	    state.pa_classes<-Int.Set.add i2 state.pa_classes
 	| Partial _ ,(Partial _ |Partial_applied) ->
-	    state.pa_classes<-Intset.remove i1 state.pa_classes
+	    state.pa_classes<-Int.Set.remove i1 state.pa_classes
 	| Partial_applied,Unknown ->
 	    r2.inductive_status<-Partial_applied
 	| Partial_applied,Partial _ ->
-	    state.pa_classes<-Intset.remove i2 state.pa_classes;
+	    state.pa_classes<-Int.Set.remove i2 state.pa_classes;
 	    r2.inductive_status<-Partial_applied
 	| Total cpl,Unknown -> r2.inductive_status<-Total cpl;
 	| Total (i,pac),Total _ -> Queue.add (i,Cmark pac) state.marks
@@ -623,7 +623,7 @@ let update t state = (* update 1 and 2 *)
       match rep.inductive_status with
 	  Partial _ ->
 	    rep.inductive_status <- Partial_applied;
-	    state.pa_classes <- Intset.remove i state.pa_classes
+	    state.pa_classes <- Int.Set.remove i state.pa_classes
 	| _ -> ()
     end;
     PacMap.iter
@@ -640,7 +640,7 @@ let update t state = (* update 1 and 2 *)
 
 let process_function_mark t rep paf state  =
   add_paf rep paf t;
-  state.terms<-Intset.union rep.lfathers state.terms
+  state.terms<-Int.Set.union rep.lfathers state.terms
 
 let process_constructor_mark t i rep pac state =
     match rep.inductive_status with
@@ -662,16 +662,16 @@ let process_constructor_mark t i rep pac state =
 	    in f cinfo.ci_nhyps opac.args pac.args
       | Partial_applied | Partial _ ->
 	  add_pac rep pac t;
-	  state.terms<-Intset.union rep.lfathers state.terms
+	  state.terms<-Int.Set.union rep.lfathers state.terms
       | Unknown ->
 	  if pac.arity = 0 then
 	    rep.inductive_status <- Total (t,pac)
 	  else
 	    begin
 	      add_pac rep pac t;
-	      state.terms<-Intset.union rep.lfathers state.terms;
+	      state.terms<-Int.Set.union rep.lfathers state.terms;
 	      rep.inductive_status <- Partial pac;
-	      state.pa_classes<- Intset.add i state.pa_classes
+	      state.pa_classes<- Int.Set.add i state.pa_classes
 	    end
 
 let process_mark t m state =
@@ -716,8 +716,8 @@ let one_step state =
 	  true
       with Queue.Empty ->
 	try
-	  let t = Intset.choose state.terms in
-	    state.terms<-Intset.remove t state.terms;
+	  let t = Int.Set.choose state.terms in
+	    state.terms<-Int.Set.remove t state.terms;
 	    update t state;
 	    true
 	with Not_found -> false
@@ -753,7 +753,7 @@ let complete_one_class state i=
     | _ -> anomaly "wrong incomplete class"
 
 let complete state =
-  Intset.iter (complete_one_class state) state.pa_classes
+  Int.Set.iter (complete_one_class state) state.pa_classes
 
 type matching_problem =
 {mp_subst : int array;
@@ -771,8 +771,8 @@ let make_fun_table state =
 	       (fun paf _ ->
 		  let elem =
 		    try PafMap.find paf !funtab
-		    with Not_found -> Intset.empty in
-		    funtab:= PafMap.add paf (Intset.add i elem) !funtab)
+		    with Not_found -> Int.Set.empty in
+		    funtab:= PafMap.add paf (Int.Set.add i elem) !funtab)
 	       rep.functions
 	 | _ -> ()) state.uf.map;
     !funtab
@@ -817,7 +817,7 @@ let do_match state res pb_stack =
 			     mp_stack=
 			      (PApp(f,rem_args),s) ::
 				(last_arg,t) :: remains} pb_stack in
-		      Intset.iter aux good_terms
+		      Int.Set.iter aux good_terms
 		  with Not_found -> ()
 
 let paf_of_patt syms = function
@@ -834,21 +834,21 @@ let init_pb_stack state =
     begin
       let good_classes =
 	match inst.qe_lhs_valid with
-	  Creates_variables -> Intset.empty
+	  Creates_variables -> Int.Set.empty
 	| Normal ->
 	    begin
 	      try
 		let paf= paf_of_patt syms inst.qe_lhs in
 		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end
 	| Trivial typ ->
 	    begin
 	      try
 		Typehash.find state.by_type typ
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end in
-	Intset.iter (fun i ->
+	Int.Set.iter (fun i ->
 		       Stack.push
 			 {mp_subst = Array.make inst.qe_nvars (-1);
 			  mp_inst=inst;
@@ -857,21 +857,21 @@ let init_pb_stack state =
     begin
       let good_classes =
 	match inst.qe_rhs_valid with
-	  Creates_variables -> Intset.empty
+	  Creates_variables -> Int.Set.empty
 	| Normal ->
 	    begin
 	      try
 		let paf= paf_of_patt syms inst.qe_rhs in
 		  PafMap.find paf funtab
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end
 	| Trivial typ ->
 	    begin
 	      try
 		Typehash.find state.by_type typ
-	      with Not_found -> Intset.empty
+	      with Not_found -> Int.Set.empty
 	    end in
-	Intset.iter (fun i ->
+	Int.Set.iter (fun i ->
 		       Stack.push
 			 {mp_subst = Array.make inst.qe_nvars (-1);
 			  mp_inst=inst;
@@ -903,7 +903,7 @@ let rec execute first_run state =
     done;
     match check_disequalities state with
 	None ->
-	  if not(Intset.is_empty state.pa_classes) then
+	  if not(Int.Set.is_empty state.pa_classes) then
 	    begin
 	      debug (str "First run was incomplete, completing ... ");
 	      complete state;
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 50f99586a..6232b126e 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -123,7 +123,7 @@ type matching_problem
 
 module PafMap: Map.S with type key = pa_fun
 
-val make_fun_table : state -> Intset.t PafMap.t
+val make_fun_table : state -> Int.Set.t PafMap.t
 
 val do_match :  state ->
     (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 3b2e42d4e..7d4d1728a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -103,7 +103,7 @@ let rec pattern_of_constr env sigma c =
 	let pargs,lrels = List.split
 	  (Array.map_to_list (pattern_of_constr env sigma) args) in
 	  PApp (pf,List.rev pargs),
-	List.fold_left Intset.union Intset.empty lrels
+	List.fold_left Int.Set.union Int.Set.empty lrels
     | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->
 	let b = Termops.pop _b in
 	let pa,sa = pattern_of_constr env sigma a in
@@ -111,11 +111,11 @@ let rec pattern_of_constr env sigma c =
 	let sort_b = sf_of env sigma b in
 	let sort_a = sf_of env sigma a in
 	  PApp(Product (sort_a,sort_b),
-	       [pa;pb]),(Intset.union sa sb)
-    | Rel i -> PVar i,Intset.singleton i
+	       [pa;pb]),(Int.Set.union sa sb)
+    | Rel i -> PVar i,Int.Set.singleton i
     | _ ->
 	let pf = decompose_term env sigma c in
-	  PApp (pf,[]),Intset.empty
+	  PApp (pf,[]),Int.Set.empty
 
 let non_trivial = function
     PVar _ -> false
@@ -129,11 +129,11 @@ let patterns_of_constr env sigma nrels term=
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
 	  let valid1 =
-	    if Intset.cardinal rels1 <> nrels then Creates_variables
+	    if Int.Set.cardinal rels1 <> nrels then Creates_variables
 	    else if non_trivial patt1 then Normal
 	    else Trivial args.(0)
 	  and valid2 =
-	    if Intset.cardinal rels2 <> nrels then Creates_variables
+	    if Int.Set.cardinal rels2 <> nrels then Creates_variables
 	    else if non_trivial patt2 then Normal
 	    else Trivial args.(0) in
 	    if valid1 <> Creates_variables
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index cc2ef96dd..6645f1d5d 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -169,7 +169,7 @@ let db_from_sign s =
 
 let rec db_from_ind dbmap i =
   if i = 0 then []
-  else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
+  else (try Int.Map.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
 
 (*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
   of a constructor corresponds to the j-th type var of the ML inductive. *)
@@ -183,11 +183,11 @@ let rec db_from_ind dbmap i =
 
 let parse_ind_args si args relmax =
   let rec parse i j = function
-    | [] -> Intmap.empty
+    | [] -> Int.Map.empty
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
       (match kind_of_term args.(i-1) with
-	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
+	 | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
@@ -493,7 +493,7 @@ and extract_type_cons env db dbmap c i =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
-	let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
+	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
 	let l = extract_type_cons env' db' dbmap d (i+1) in
 	(extract_type env db 0 t []) :: l
     | _ -> []
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index b53fec23e..18c3f840e 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -171,12 +171,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))
@@ -731,14 +731,14 @@ 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 s = try Hashtbl.find h e with Not_found -> Int.Set.empty in
+    Hashtbl.replace h e (Int.Set.add i s)
   in
   let max e0 =
-    let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
+    let len = ref 0 and lst = ref Int.Set.empty and elm = ref e0 in
     Hashtbl.iter
       (fun e s ->
-	 let n = Intset.cardinal s in
+	 let n = Int.Set.cardinal s in
 	 if n > !len then begin len := n; lst := s; elm := e end)
       h;
     (!elm,!lst)
@@ -766,7 +766,7 @@ 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
+    let n = Int.Set.cardinal br_set in
     if n = 0 then None
     else if Array.length br >= 2 && n < 2 then None
     else Some (br_factor, br_set)
@@ -945,7 +945,7 @@ and simpl_case o typ br e =
       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.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) ->
@@ -954,7 +954,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.filteri (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)
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index f823cfa55..93f84687e 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -46,12 +46,12 @@ let unif t1 t2=
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Intset.is_empty (free_rels t) &&
+		if Int.Set.is_empty (free_rels t) &&
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Intset.is_empty (free_rels t) &&
+		if Int.Set.is_empty (free_rels t) &&
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f431e04d8..c129306d2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -267,12 +267,12 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	let t2 = destRel t2  in
 	begin
 	  try
-	    let t1' = Intmap.find t2 sub in
+	    let t1' = Int.Map.find t2 sub in
 	    if not (eq_constr t1 t1') then nochange "twice bound variable";
 	    sub
 	  with Not_found ->
 	    assert (closed0 t1);
-	    Intmap.add t2 t1 sub
+	    Int.Map.add t2 t1 sub
 	end
       else if isAppConstruct t1 && isAppConstruct t2
       then
@@ -286,14 +286,14 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       else
 	if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2)  "cannot solve (diff)"
     in
-    let sub = compute_substitution Intmap.empty (snd t1) (snd t2) in
+    let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in
     let sub = compute_substitution sub (fst t1) (fst t2) in
     let end_of_type_with_pop = Termops.pop end_of_type in (*the equation will be removed *)
     let new_end_of_type =
       (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4
 	 Can be safely replaced by the next comment for Ocaml >= 3.08.4
       *)
-      let sub' = Intmap.fold (fun i t acc -> (i,t)::acc) sub [] in
+      let sub' = Int.Map.fold (fun i t acc -> (i,t)::acc) sub [] in
       let sub'' = List.sort (fun (x,_) (y,_) -> Pervasives.compare x y) sub' in
       List.fold_left (fun end_of_type (i,t)  -> lift 1 (substnl  [t] (i-1) end_of_type))
 	end_of_type_with_pop
@@ -309,7 +309,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       List.fold_left_i
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
-	     let witness = Intmap.find i sub in
+	     let witness = Int.Map.find i sub in
 	     if b' <> None then anomaly "can not redefine a rel!";
 	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
 	   with Not_found  ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0dceecf4f..2fdf62d26 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -297,8 +297,8 @@ let rec hdMatchSub inu (test: constr -> bool) : fapp_info list =
   else
     let f,args = decompose_app inu in
     let freeset = Termops.free_rels inu in
-    let max_rel = try Util.Intset.max_elt freeset with Not_found -> -1 in
-    {fname = f; largs = args; free = Util.Intset.is_empty freeset;
+    let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in
+    {fname = f; largs = args; free = Int.Set.is_empty freeset;
     max_rel = max_rel; onlyvars = List.for_all isVar args }
     ::subres
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 6a7a588d4..22da1a966 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -18,7 +18,7 @@ let is_rec_info scheme_info =
 	it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in
       let free_rels_in_br = Termops.free_rels new_branche in
       let max = min + scheme_info.Tactics.npredicates in
-      Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br
+      Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br
     )
   in
   List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 20ec17269..5cb97d4bd 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -65,8 +65,8 @@ type form=
 module Fmap=Map.Make(struct type t=form let compare=compare end)
 
 type sequent =
-    {rev_hyps: form Intmap.t;
-     norev_hyps: form Intmap.t;
+    {rev_hyps: form Int.Map.t;
+     norev_hyps: form Int.Map.t;
      size:int;
      left:int Fmap.t;
      right:(int*form) list Fmap.t;
@@ -127,16 +127,16 @@ let add_step s sub =
 type 'a with_deps =
     {dep_it:'a;
      dep_goal:bool;
-     dep_hyps:Intset.t}
+     dep_hyps:Int.Set.t}
 
 type slice=
     {proofs_done:proof list;
      proofs_todo:sequent with_deps list;
      step:rule;
      needs_goal:bool;
-     needs_hyps:Intset.t;
+     needs_hyps:Int.Set.t;
      changes_goal:bool;
-     creates_hyps:Intset.t}
+     creates_hyps:Int.Set.t}
 
 type state =
     Complete of proof
@@ -161,25 +161,25 @@ let rec fill stack proof =
 	  !pruning &&
 	  slice.proofs_done=[] &&
 	  not (slice.changes_goal && proof.dep_goal) &&
-	  not (Intset.exists
-		 (fun i -> Intset.mem i proof.dep_hyps)
+	  not (Int.Set.exists
+		 (fun i -> Int.Set.mem i proof.dep_hyps)
 		 slice.creates_hyps)
 	then
 	  begin
 	    s_info.pruned_steps<-s_info.pruned_steps+1;
 	    s_info.pruned_branches<- s_info.pruned_branches +
 	    List.length slice.proofs_todo;
-	    let created_here=Intset.cardinal slice.creates_hyps in
+	    let created_here=Int.Set.cardinal slice.creates_hyps in
 	      s_info.pruned_hyps<-s_info.pruned_hyps+
 	      List.fold_left
-		(fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps)
+		(fun sum dseq -> sum + Int.Set.cardinal dseq.dep_hyps)
 		created_here slice.proofs_todo;
-	    fill super (pop (Intset.cardinal slice.creates_hyps) proof)
+	    fill super (pop (Int.Set.cardinal slice.creates_hyps) proof)
 	  end
 	else
 	  let dep_hyps=
-	    Intset.union slice.needs_hyps
-	      (Intset.diff proof.dep_hyps slice.creates_hyps) in
+	    Int.Set.union slice.needs_hyps
+	      (Int.Set.diff proof.dep_hyps slice.creates_hyps) in
 	  let dep_goal=
 	    slice.needs_goal ||
 	    ((not slice.changes_goal) && proof.dep_goal) in
@@ -226,7 +226,7 @@ let append stack (step,subgoals) =
 let embed seq=
   {dep_it=seq;
    dep_goal=false;
-   dep_hyps=Intset.empty}
+   dep_hyps=Int.Set.empty}
 
 let change_goal seq gl=
     {seq with
@@ -261,7 +261,7 @@ let add_hyp seqwd f=
 	     cnx=cnx}
       | Conjunct (_,_) | Disjunct (_,_) ->
 	  {seq with
-	     rev_hyps=Intmap.add num f seq.rev_hyps;
+	     rev_hyps=Int.Map.add num f seq.rev_hyps;
 	     size=num;
 	     left=left;
 	     right=right;
@@ -276,14 +276,14 @@ let add_hyp seqwd f=
 	    match f1 with
 		Conjunct (_,_) | Disjunct (_,_) ->
 		  {seq with
-		     rev_hyps=Intmap.add num f seq.rev_hyps;
+		     rev_hyps=Int.Map.add num f seq.rev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
 		     cnx=ncnx}
 	      | Arrow(_,_) ->
 		  {seq with
-		     norev_hyps=Intmap.add num f seq.norev_hyps;
+		     norev_hyps=Int.Map.add num f seq.norev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
@@ -296,13 +296,13 @@ let add_hyp seqwd f=
 		     cnx=ncnx} in
     {seqwd with
        dep_it=nseq;
-       dep_hyps=Intset.add num seqwd.dep_hyps}
+       dep_hyps=Int.Set.add num seqwd.dep_hyps}
 
 exception Here_is of (int*form)
 
 let choose m=
   try
-    Intmap.iter (fun i f -> raise (Here_is (i,f))) m;
+    Int.Map.iter (fun i f -> raise (Here_is (i,f))) m;
     raise Not_found
   with
       Here_is (i,f) -> (i,f)
@@ -313,11 +313,11 @@ let search_or seq=
       Disjunct (f1,f2) ->
 	[{dep_it = SI_Or_l;
 	  dep_goal = true;
-	  dep_hyps = Intset.empty},
+	  dep_hyps = Int.Set.empty},
 	 [change_goal (embed seq) f1];
 	 {dep_it = SI_Or_r;
 	  dep_goal = true;
-	  dep_hyps = Intset.empty},
+	  dep_hyps = Int.Set.empty},
 	 [change_goal (embed seq) f2]]
     | _ -> []
 
@@ -327,11 +327,11 @@ let search_norev seq=
     match f with
 	Arrow (Arrow (f1,f2),f3) ->
 	  let nseq =
-	    {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in
+	    {seq with norev_hyps=Int.Map.remove i seq.norev_hyps} in
 	    goals:=
 	      ({dep_it=SD_Arrow(i);
 		dep_goal=false;
-		dep_hyps=Intset.singleton i},
+		dep_hyps=Int.Set.singleton i},
 	       [add_hyp
 		  (add_hyp
 		     (change_goal (embed nseq) f2)
@@ -339,7 +339,7 @@ let search_norev seq=
 		  f1;
 		add_hyp (embed nseq) f3]):: !goals
       | _ -> anomaly "search_no_rev: can't happen" in
-    Intmap.iter add_one seq.norev_hyps;
+    Int.Map.iter add_one seq.norev_hyps;
     List.rev !goals
 
 let search_in_rev_hyps seq=
@@ -348,8 +348,8 @@ let search_in_rev_hyps seq=
     let make_step step=
       {dep_it=step;
        dep_goal=false;
-       dep_hyps=Intset.singleton i} in
-    let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in
+       dep_hyps=Int.Set.singleton i} in
+    let nseq={seq with rev_hyps=Int.Map.remove i seq.rev_hyps} in
       match f with
 	  Conjunct (f1,f2) ->
 	    [make_step (SE_And(i)),
@@ -374,27 +374,27 @@ let search_rev seq=
 	  match f1 with
 	      Conjunct (_,_) | Disjunct (_,_) ->
 		{seq with cnx=next;
-		   rev_hyps=Intmap.remove j seq.rev_hyps}
+		   rev_hyps=Int.Map.remove j seq.rev_hyps}
 	    | Arrow (_,_) ->
 		{seq with cnx=next;
-		   norev_hyps=Intmap.remove j seq.norev_hyps}
+		   norev_hyps=Int.Map.remove j seq.norev_hyps}
 	    | _ ->
 		{seq with cnx=next} in
 	  [{dep_it=SE_Arrow(i,j);
 	    dep_goal=false;
-	    dep_hyps=Intset.add i (Intset.singleton j)},
+	    dep_hyps=Int.Set.add i (Int.Set.singleton j)},
 	   [add_hyp (embed nseq) f2]]
     | [] ->
 	match seq.gl with
 	    Arrow (f1,f2) ->
 	      [{dep_it=SI_Arrow;
 		dep_goal=true;
-		dep_hyps=Intset.empty},
+		dep_hyps=Int.Set.empty},
 	       [add_hyp (change_goal (embed seq) f2) f1]]
 	  | Conjunct (f1,f2) ->
 	      [{dep_it=SI_And;
 		dep_goal=true;
-		dep_hyps=Intset.empty},[change_goal (embed seq) f1;
+		dep_hyps=Int.Set.empty},[change_goal (embed seq) f1;
 					change_goal (embed seq) f2]]
 	  | _ -> search_in_rev_hyps seq
 
@@ -403,18 +403,18 @@ let search_all seq=
       Some i ->
 	[{dep_it=SE_False (i);
 	  dep_goal=false;
-	  dep_hyps=Intset.singleton i},[]]
+	  dep_hyps=Int.Set.singleton i},[]]
     | None ->
 	try
 	  let ax = Fmap.find seq.gl seq.left in
 	    [{dep_it=SAx (ax);
 	      dep_goal=true;
-	      dep_hyps=Intset.singleton ax},[]]
+	      dep_hyps=Int.Set.singleton ax},[]]
 	with Not_found -> search_rev seq
 
 let bare_sequent = embed
-		     {rev_hyps=Intmap.empty;
-		      norev_hyps=Intmap.empty;
+		     {rev_hyps=Int.Map.empty;
+		      norev_hyps=Int.Map.empty;
 		      size=0;
 		      left=Fmap.empty;
 		      right=Fmap.empty;
@@ -466,7 +466,7 @@ let pr_form f = pp_form f
 
 let pp_intmap map =
   let pp=ref (str "") in
-   Intmap.iter (fun i obj -> pp:= (!pp ++
+   Int.Map.iter (fun i obj -> pp:= (!pp ++
 		pp_form obj ++ cut ())) map;
     str "{ " ++ v 0 (!pp) ++ str " }"
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ab9ed2993..c02dbba23 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1518,7 +1518,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	  (rel_context extenv) in
       let rel_filter =
 	List.map (fun a -> not (isRel a) || dependent a u
-                           || Intset.mem (destRel a) depvl) inst in
+                           || Int.Set.mem (destRel a) depvl) inst in
       let named_filter =
 	List.map (fun (id,_,_) -> dependent (mkVar id) u)
 	  (named_context extenv) in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 5303252c8..3cf0c50ba 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -594,7 +594,7 @@ let filter_possible_projections c ty ctxt args =
     (* Here we make an approximation, for instance, we could also be *)
     (* interested in finding a term u convertible to c such that a occurs *)
     (* in u *)
-    isRel a && Intset.mem (destRel a) fv1 ||
+    isRel a && Int.Set.mem (destRel a) fv1 ||
     isVar a && Idset.mem (destVar a) fv2 ||
     Idset.mem id tyvars)
     ctxt args
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 4996f86c2..b82f18da7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -456,15 +456,15 @@ let compute_rel_aliases var_aliases rels =
          | Var id' ->
              let aliases_of_n =
                try Idmap.find id' var_aliases with Not_found -> [] in
-             Intmap.add n (aliases_of_n@[t]) aliases
+             Int.Map.add n (aliases_of_n@[t]) aliases
          | Rel p ->
              let aliases_of_n =
-               try Intmap.find (p+n) aliases with Not_found -> [] in
-             Intmap.add n (aliases_of_n@[mkRel (p+n)]) aliases
+               try Int.Map.find (p+n) aliases with Not_found -> [] in
+             Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
          | _ ->
-             Intmap.add n [lift n t] aliases)
+             Int.Map.add n [lift n t] aliases)
      | None -> aliases))
-         rels (List.length rels,Intmap.empty))
+         rels (List.length rels,Int.Map.empty))
 
 let make_alias_map env =
   (* We compute the chain of aliases for each var and rel *)
@@ -475,11 +475,11 @@ let make_alias_map env =
 let lift_aliases n (var_aliases,rel_aliases as aliases) =
   if Int.equal n 0 then aliases else
   (var_aliases,
-   Intmap.fold (fun p l -> Intmap.add (p+n) (List.map (lift n) l))
-     rel_aliases Intmap.empty)
+   Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
+     rel_aliases Int.Map.empty)
 
 let get_alias_chain_of aliases x = match kind_of_term x with
-  | Rel n -> (try Intmap.find n (snd aliases) with Not_found -> [])
+  | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
   | Var id -> (try Idmap.find id (fst aliases) with Not_found -> [])
   | _ -> []
 
@@ -496,12 +496,12 @@ let normalize_alias aliases x =
   | None -> x
 
 let normalize_alias_var var_aliases id =
-  destVar (normalize_alias (var_aliases,Intmap.empty) (mkVar id))
+  destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id))
 
 let extend_alias (_,b,_) (var_aliases,rel_aliases) =
   let rel_aliases =
-    Intmap.fold (fun n l -> Intmap.add (n+1) (List.map (lift 1) l))
-      rel_aliases Intmap.empty in
+    Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
+      rel_aliases Int.Map.empty in
   let rel_aliases =
     match b with
     | Some t ->
@@ -509,13 +509,13 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
         | Var id' ->
             let aliases_of_binder =
               try Idmap.find id' var_aliases with Not_found -> [] in
-	    Intmap.add 1 (aliases_of_binder@[t]) rel_aliases
+	    Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases
         | Rel p ->
             let aliases_of_binder =
-              try Intmap.find (p+1) rel_aliases with Not_found -> [] in
-	    Intmap.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
+              try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
+	    Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
         | _ ->
-            Intmap.add 1 [lift 1 t] rel_aliases)
+            Int.Map.add 1 [lift 1 t] rel_aliases)
     | None -> rel_aliases in
   (var_aliases, rel_aliases)
 
@@ -545,14 +545,14 @@ let rec expand_vars_in_term_using aliases t = match kind_of_term t with
 let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
-  let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
-  let cache_rel = ref Intset.empty and cache_var = ref Idset.empty in
+  let acc1 = ref Int.Set.empty and acc2 = ref Idset.empty in
+  let cache_rel = ref Int.Set.empty and cache_var = ref Idset.empty in
   let is_in_cache depth = function
-    | Rel n -> Intset.mem (n-depth) !cache_rel
+    | Rel n -> Int.Set.mem (n-depth) !cache_rel
     | Var s -> Idset.mem s !cache_var
     | _ -> false in
   let put_in_cache depth = function
-    | Rel n -> cache_rel := Intset.add (n-depth) !cache_rel
+    | Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel
     | Var s -> cache_var := Idset.add s !cache_var
     | _ -> () in
   let rec frec (aliases,depth) c =
@@ -563,7 +563,7 @@ let free_vars_and_rels_up_alias_expansion aliases c =
       let c = expansion_of_var aliases c in
         match kind_of_term c with
         | Var id -> acc2 := Idset.add id !acc2
-        | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
+        | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
         acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
@@ -729,7 +729,7 @@ let get_actual_deps aliases l t =
     List.filter (fun c ->
       match kind_of_term c with
       | Var id -> Idset.mem id fv_ids
-      | Rel n -> Intset.mem n fv_rels
+      | Rel n -> Int.Set.mem n fv_rels
       | _ -> assert false) l
 
 let remove_instance_local_defs evd evk args =
@@ -1373,7 +1373,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
   | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
   | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Idset.mem id fv_ids
-  | Rel n -> n <= k || Intset.mem n fv_rels
+  | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) true
 
@@ -1381,7 +1381,7 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
   let t = expansion_of_var aliases t in
   match kind_of_term t with
   | Var id -> Idset.mem id fv_ids
-  | Rel n -> n <= k || Intset.mem n fv_rels
+  | Rel n -> n <= k || Int.Set.mem n fv_rels
   | _ -> is_constrainable_in k (ev,fvs) t
 
 let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
@@ -1800,14 +1800,14 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 let evars_of_term c =
   let rec evrec acc c =
     match kind_of_term c with
-    | Evar (n, l) -> Intset.add n (Array.fold_left evrec acc l)
+    | Evar (n, l) -> Int.Set.add n (Array.fold_left evrec acc l)
     | _ -> fold_constr evrec acc c
   in
-  evrec Intset.empty c
+  evrec Int.Set.empty c
 
 (* spiwack: a few functions to gather evars on which goals depend. *)
 let queue_set q is_dependent set =
-  Intset.iter (fun a -> Queue.push (is_dependent,a) q) set
+  Int.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
 let queue_term q is_dependent c =
   queue_set q is_dependent (evars_of_term c)
 
@@ -1824,7 +1824,7 @@ let process_dependent_evar q acc evm is_dependent e =
   end (Environ.named_context_of_val evi.evar_hyps);
   match evi.evar_body with
   | Evar_empty ->
-      if is_dependent then Intmap.add e None acc else acc
+      if is_dependent then Int.Map.add e None acc else acc
   | Evar_defined b ->
       let subevars = evars_of_term b in
       (* evars appearing in the definition of an evar [e] are marked
@@ -1832,14 +1832,14 @@ let process_dependent_evar q acc evm is_dependent e =
          non-dependent goal, then, unless they are reach from another
          path, these evars are just other non-dependent goals. *)
       queue_set q is_dependent subevars;
-      if is_dependent then Intmap.add e (Some subevars) acc else acc
+      if is_dependent then Int.Map.add e (Some subevars) acc else acc
 
 let gather_dependent_evars q evm =
-  let acc = ref Intmap.empty in
+  let acc = ref Int.Map.empty in
   while not (Queue.is_empty q) do
     let (is_dependent,e) = Queue.pop q in
     (* checks if [e] has already been added to [!acc] *)
-    begin if not (Intmap.mem e !acc) then
+    begin if not (Int.Map.mem e !acc) then
         acc := process_dependent_evar q !acc evm is_dependent e  
     end
   done;
@@ -1855,15 +1855,15 @@ let gather_dependent_evars evm l =
 let evars_of_named_context nc =
   List.fold_right (fun (_, b, t) s ->
     Option.fold_left (fun s t ->
-      Intset.union s (evars_of_term t))
-      (Intset.union s (evars_of_term t)) b)
-    nc Intset.empty
+      Int.Set.union s (evars_of_term t))
+      (Int.Set.union s (evars_of_term t)) b)
+    nc Int.Set.empty
 
 let evars_of_evar_info evi =
-  Intset.union (evars_of_term evi.evar_concl)
-    (Intset.union
+  Int.Set.union (evars_of_term evi.evar_concl)
+    (Int.Set.union
 	(match evi.evar_body with
-	| Evar_empty -> Intset.empty
+	| Evar_empty -> Int.Set.empty
 	| Evar_defined b -> evars_of_term b)
 	(evars_of_named_context (named_context_of_val evi.evar_hyps)))
 
@@ -1878,25 +1878,25 @@ let undefined_evars_of_term evd t =
       | Evar (n, l) ->
 	let acc = Array.fold_left evrec acc l in
 	(try match (Evd.find evd n).evar_body with
-	  | Evar_empty -> Intset.add n acc
+	  | Evar_empty -> Int.Set.add n acc
 	  | Evar_defined c -> evrec acc c
 	 with Not_found -> anomaly "undefined_evars_of_term: evar not found")
       | _ -> fold_constr evrec acc c
   in
-  evrec Intset.empty t
+  evrec Int.Set.empty t
 
 let undefined_evars_of_named_context evd nc =
   List.fold_right (fun (_, b, t) s ->
     Option.fold_left (fun s t ->
-      Intset.union s (undefined_evars_of_term evd t))
-      (Intset.union s (undefined_evars_of_term evd t)) b)
-    nc Intset.empty
+      Int.Set.union s (undefined_evars_of_term evd t))
+      (Int.Set.union s (undefined_evars_of_term evd t)) b)
+    nc Int.Set.empty
 
 let undefined_evars_of_evar_info evd evi =
-  Intset.union (undefined_evars_of_term evd evi.evar_concl)
-    (Intset.union
+  Int.Set.union (undefined_evars_of_term evd evi.evar_concl)
+    (Int.Set.union
        (match evi.evar_body with
-	 | Evar_empty -> Intset.empty
+	 | Evar_empty -> Int.Set.empty
 	 | Evar_defined b -> undefined_evars_of_term evd b)
        (undefined_evars_of_named_context evd
 	  (named_context_of_val evi.evar_hyps)))
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a4f9ff486..fb53654de 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -118,10 +118,10 @@ val solve_pattern_eqn : env -> constr list -> constr -> constr
     contained in the object, including defined evars *)
 
 
-val evars_of_term : constr -> Intset.t
+val evars_of_term : constr -> Int.Set.t
 
-val evars_of_named_context : named_context -> Intset.t
-val evars_of_evar_info : evar_info -> Intset.t
+val evars_of_named_context : named_context -> Int.Set.t
+val evars_of_evar_info : evar_info -> Int.Set.t
 
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
     as dependent_evars and goals (these may overlap). A goal is an
@@ -132,16 +132,16 @@ val evars_of_evar_info : evar_info -> Intset.t
     associating to each dependent evar [None] if it has no (partial)
     definition or [Some s] if [s] is the list of evars appearing in
     its (partial) definition. *)
-val gather_dependent_evars : evar_map -> evar list -> (Intset.t option) Intmap.t
+val gather_dependent_evars : evar_map -> evar list -> (Int.Set.t option) Int.Map.t
 
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
     [nf_evar]. *)
 
-val undefined_evars_of_term : evar_map -> constr -> Intset.t
-val undefined_evars_of_named_context : evar_map -> named_context -> Intset.t
-val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
+val undefined_evars_of_term : evar_map -> constr -> Int.Set.t
+val undefined_evars_of_named_context : evar_map -> named_context -> Int.Set.t
+val undefined_evars_of_evar_info : evar_map -> evar_info -> Int.Set.t
 
 (** {6 Value/Type constraints} *)
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 8849f1769..8722516bb 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -80,8 +80,8 @@ let eq_evar_info ei1 ei2 =
    - evar_map (exported)
 *)
 
-module ExistentialMap = Intmap
-module ExistentialSet = Intset
+module ExistentialMap = Int.Map
+module ExistentialSet = Int.Set
 
 (* This exception is raised by *.existential_value *)
 exception NotInstantiatedEvar
@@ -244,16 +244,16 @@ end
 
 type 'a freelisted = {
   rebus : 'a;
-  freemetas : Intset.t }
+  freemetas : Int.Set.t }
 
 (* Collects all metavars appearing in a constr *)
 let metavars_of c =
   let rec collrec acc c =
     match kind_of_term c with
-      | Meta mv -> Intset.add mv acc
+      | Meta mv -> Int.Set.add mv acc
       | _         -> fold_constr collrec acc c
   in
-  collrec Intset.empty c
+  collrec Int.Set.empty c
 
 let mk_freelisted c =
   { rebus = c; freemetas = metavars_of c }
@@ -308,11 +308,11 @@ let clb_name = function
 
 (***********************)
 
-module Metaset = Intset
+module Metaset = Int.Set
 
 let meta_exists p s = Metaset.fold (fun x b -> b || (p x)) s false
 
-module Metamap = Intmap
+module Metamap = Int.Map
 
 let metamap_to_list m =
   Metamap.fold (fun n v l -> (n,v)::l) m []
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index a456d08cc..9f4badd22 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -79,7 +79,7 @@ let build_lambda toabstract stk (m : constr) =
   let rec buildrec m p_0 p_1 = match p_0,p_1 with
     | (_, []) -> m
     | (n, (_,na,t)::tl) ->
-	if Intset.mem n toabstract then
+	if Int.Set.mem n toabstract then
           buildrec (mkLambda (na,t,m)) (n+1) tl
         else
 	  buildrec (lift (-1) m) (n+1) tl
@@ -126,7 +126,7 @@ let merge_binding allow_bound_rels stk n cT subst =
       (* Optimization *)
       ([],cT)
     else
-      let frels = Intset.elements (free_rels cT) in
+      let frels = Int.Set.elements (free_rels cT) in
       let frels = List.filter (fun i -> i <= depth) frels in
       if allow_bound_rels then
 	let frels = Sort.list (<) frels in
@@ -148,12 +148,12 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
     match p,kind_of_term cT with
       | PSoApp (n,args),m ->
         let fold accu = function
-        | PRel n -> Intset.add n accu
+        | PRel n -> Int.Set.add n accu
         | _ -> error "Only bound indices allowed in second order pattern matching."
         in
-        let relargs = List.fold_left fold Intset.empty args in
+        let relargs = List.fold_left fold Int.Set.empty args in
         let frels = free_rels cT in
-        if Intset.subset frels relargs then
+        if Int.Set.subset frels relargs then
           constrain n ([], build_lambda relargs stk cT) subst
         else
           raise PatternMatchingFailure
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8e4351deb..c7819e134 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -390,17 +390,17 @@ and pats_of_glob_branches loc metas vars ind brs =
       | _ ->
         err loc (Pp.str "All constructors must be in the same inductive type.")
       in
-      if Intset.mem (j-1) indexes then
+      if Int.Set.mem (j-1) indexes then
 	err loc
           (str "No unique branch for " ++ int j ++ str"-th constructor.");
       let lna = List.map get_arg lv in
       let vars' = List.rev lna @ vars in
       let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
-      let ext,pats = get_pat (Intset.add (j-1) indexes) brs in
+      let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
       ext, ((j-1, List.length lv, pat) :: pats)
     | (loc,_,_,_) :: _ -> err loc (Pp.str "Non supported pattern.")
   in
-  get_pat Intset.empty brs
+  get_pat Int.Set.empty brs
 
 let pattern_of_glob_constr c =
   let metas = ref [] in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index fc78b0dca..6c2f8f189 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -198,7 +198,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
     raise Elimconst;
   List.iteri (fun i t_i ->
     if not (List.mem_assoc (i+1) li) then
-      let fvs = List.map ((+) (i+1)) (Intset.elements (free_rels t_i)) in
+      let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels t_i)) in
       match List.intersect fvs reversible_rels with
       | [] -> ()
       | _ -> raise Elimconst)
@@ -372,7 +372,7 @@ let vfun = id_of_string"_eliminator_function_"
 let substl_with_function subst constr =
   let cnt = ref 0 in
   let evd = ref Evd.empty in
-  let minargs = ref Intmap.empty in
+  let minargs = ref Int.Map.empty in
   let v = Array.of_list subst in
   let rec subst_total k c =
     match kind_of_term c with
@@ -386,7 +386,7 @@ let substl_with_function subst constr =
                       (val_of_named_context
                         [(vfx,None,dummy);(vfun,None,dummy)])
                       dummy);
-                  minargs := Intmap.add !cnt min !minargs;
+                  minargs := Int.Map.add !cnt min !minargs;
                   lift k (mkEvar(!cnt,[|fx;ref|]))
               | (fx,None) -> lift k fx
           else mkRel (i - Array.length v)
@@ -406,8 +406,8 @@ let solve_arity_problem env sigma fxminargs c =
     let c' = whd_betaiotazeta sigma c in
     let (h,rcargs) = decompose_app c' in
     match kind_of_term h with
-        Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) ->
-          let minargs = Intmap.find i fxminargs in
+        Evar(i,_) when Int.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
+          let minargs = Int.Map.find i fxminargs in
           if List.length rcargs < minargs then
             if strict then set_fix i
             else raise Partial;
@@ -434,7 +434,7 @@ let substl_checking_arity env subst c =
      the other ones are replaced by the function symbol *)
   let rec nf_fix c =
     match kind_of_term c with
-        Evar(i,[|fx;f|] as ev) when Intmap.mem i minargs ->
+        Evar(i,[|fx;f|] as ev) when Int.Map.mem i minargs ->
           (match Evd.existential_opt_value sigma' ev with
               Some c' -> c'
             | None -> f)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 973f85818..4a267dd7e 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -544,10 +544,10 @@ let occur_var_in_decl env hyp (_,c,typ) =
 
 let free_rels m =
   let rec frec depth acc c = match kind_of_term c with
-    | Rel n       -> if n >= depth then Intset.add (n-depth+1) acc else acc
+    | Rel n       -> if n >= depth then Int.Set.add (n-depth+1) acc else acc
     | _ -> fold_constr_with_binders succ frec depth acc c
   in
-  frec 1 Intset.empty m
+  frec 1 Int.Set.empty m
 
 (* collects all metavar occurences, in left-to-right order, preserving
  * repetitions and all. *)
@@ -912,18 +912,18 @@ let split_app c = match kind_of_term c with
 	c::(Array.to_list prev), last
   | _ -> assert false
 
-type subst = (rel_context*constr) Intmap.t
+type subst = (rel_context*constr) Int.Map.t
 
 exception CannotFilter
 
 let filtering env cv_pb c1 c2 =
-  let evm = ref Intmap.empty in
+  let evm = ref Int.Map.empty in
   let define cv_pb e1 ev c1 =
-    try let (e2,c2) = Intmap.find ev !evm in
+    try let (e2,c2) = Int.Map.find ev !evm in
     let shift = List.length e1 - List.length e2 in
     if constr_cmp cv_pb c1 (lift shift c2) then () else raise CannotFilter
     with Not_found ->
-      evm := Intmap.add ev (e1,c1) !evm
+      evm := Int.Map.add ev (e1,c1) !evm
   in
   let rec aux env cv_pb c1 c2 =
     match kind_of_term c1, kind_of_term c2 with
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 4d9ce4969..096cdbcbb 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -108,7 +108,7 @@ val occur_var : env -> identifier -> types -> bool
 val occur_var_in_decl :
   env ->
   identifier -> 'a * types option * types -> bool
-val free_rels : constr -> Intset.t
+val free_rels : constr -> Int.Set.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val count_occurrences : constr -> constr -> int
@@ -207,7 +207,7 @@ exception CannotFilter
    (context,term), or raises [CannotFilter].
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
-type subst = (rel_context*constr) Intmap.t
+type subst = (rel_context*constr) Int.Map.t
 val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
 
 val decompose_prod_letin : constr -> int * rel_context * constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bf0f47a32..facc243e2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -419,13 +419,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| Evar (evk,_ as ev), _
             when not (ExistentialSet.mem evk flags.frozen_evars) ->
 	    let cmvars = free_rels cM and cnvars = free_rels cN in
-	      if Intset.subset cnvars cmvars then
+	      if Int.Set.subset cnvars cmvars then
 		sigma,metasubst,((curenv,ev,cN)::evarsubst)
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| _, Evar (evk,_ as ev)
             when not (ExistentialSet.mem evk flags.frozen_evars) ->
 	    let cmvars = free_rels cM and cnvars = free_rels cN in
-	      if Intset.subset cmvars cnvars then
+	      if Int.Set.subset cmvars cnvars then
 		sigma,metasubst,((curenv,ev,cM)::evarsubst)
 	      else error_cannot_unify_local curenv sigma (m,n,cN)
 	| Sort s1, Sort s2 ->
diff --git a/printing/printer.ml b/printing/printer.ml
index a5f884d46..4f09460d8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -336,13 +336,13 @@ let emacs_print_dependent_evars sigma seeds =
   let evars () =
     let evars = Evarutil.gather_dependent_evars sigma seeds in
     let evars =
-      Intmap.fold begin fun e i s ->
+      Int.Map.fold begin fun e i s ->
 	let e' = str (string_of_existential e) in
 	match i with
 	| None -> s ++ str" " ++ e' ++ str " open,"
 	| Some i ->
 	  s ++ str " " ++ e' ++ str " using " ++
-	    Intset.fold begin fun d s ->
+	    Int.Set.fold begin fun d s ->
 	      str (string_of_existential d) ++ str " " ++ s
 	    end i (str ",")
       end evars (str "")
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a4b914525..bcd51fe2b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -114,7 +114,7 @@ let focus_sublist i j l =
   let (left,sub_right) = list_goto (i-1) l in
   let (sub, right) = 
     try 
-      Util.List.chop (j-i+1) sub_right 
+      List.chop (j-i+1) sub_right 
     with Failure "list_chop" -> 
       Errors.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal")
   in
@@ -482,7 +482,7 @@ module V82 = struct
 
   let top_evars { initial=initial } =
     let evars_of_initial (c,_) =
-      Util.Intset.elements (Evarutil.evars_of_term c)
+      Int.Set.elements (Evarutil.evars_of_term c)
     in
     List.flatten (List.map evars_of_initial initial)
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 49841ecfa..ecc0930c1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -823,7 +823,7 @@ let prepare_hint env (sigma,c) =
       (* We skip the test whether args is the identity or not *)
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
-      if not (Intset.is_empty (free_rels t)) then
+      if not (Int.Set.is_empty (free_rels t)) then
 	error "Hints with holes dependent on a bound variable not supported.";
       if occur_existential t then
 	(* Not clever enough to construct dependency graph of evars *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a18992f70..8e0dbc6ef 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -403,7 +403,7 @@ let isProp env sigma concl =
 
 let needs_backtrack only_classes env evd oev concl =
   if Option.is_empty oev || isProp env evd concl then
-    not (Intset.is_empty (Evarutil.evars_of_term concl))
+    not (Int.Set.is_empty (Evarutil.evars_of_term concl))
   else true
 
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
@@ -530,19 +530,19 @@ let resolve_all_evars_once debug limit p evd =
     Beware of the imperative effects on the partition structure,
     it should not be shared, but only used locally. *)
 
-module Intpart = Unionfind.Make(Intset)(Intmap)
+module Intpart = Unionfind.Make(Int.Set)(Int.Map)
 
 let deps_of_constraints cstrs evm p =
   List.iter (fun (_, _, x, y) ->
     let evx = Evarutil.undefined_evars_of_term evm x in
     let evy = Evarutil.undefined_evars_of_term evm y in
-    Intpart.union_set (Intset.union evx evy) p)
+    Intpart.union_set (Int.Set.union evx evy) p)
     cstrs
 
 let evar_dependencies evm p =
   Evd.fold_undefined
     (fun ev evi _ ->
-      let evars = Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+      let evars = Int.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
       in Intpart.union_set evars p)
     evm ()
 
@@ -577,7 +577,7 @@ let split_evars evm =
 let evars_in_comp comp evm =
   try
     evars_reset_evd 
-      (Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
+      (Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
 	 comp Evd.empty) evm
   with Not_found -> assert false
 
@@ -595,7 +595,7 @@ let is_inference_forced p evd ev =
   with Not_found -> assert false
 
 let is_mandatory p comp evd =
-  Intset.exists (is_inference_forced p evd) comp
+  Int.Set.exists (is_inference_forced p evd) comp
 
 (** In case of unsatisfiable constraints, build a nice error message *)
 
@@ -661,8 +661,8 @@ let revert_resolvability oevd evd =
 exception Unresolved
 
 let resolve_all_evars debug m env p oevd do_split fail =
-  let split = if do_split then split_evars oevd else [Intset.empty] in
-  let in_comp comp ev = if do_split then Intset.mem ev comp else true
+  let split = if do_split then split_evars oevd else [Int.Set.empty] in
+  let in_comp comp ev = if do_split then Int.Set.mem ev comp else true
   in
   let rec docomp evd = function
     | [] -> revert_resolvability oevd evd
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ca54436a0..8d457d9f4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -878,7 +878,7 @@ let minimal_free_rels env sigma (c,cty) =
   let cty_rels = free_rels cty in
   let cty' = simpl env sigma cty in
   let rels' = free_rels cty' in
-  if Intset.subset cty_rels rels' then
+  if Int.Set.subset cty_rels rels' then
     (cty,cty_rels)
   else
     (cty',rels')
@@ -888,10 +888,10 @@ let minimal_free_rels env sigma (c,cty) =
 let minimal_free_rels_rec env sigma =
   let rec minimalrec_free_rels_rec prev_rels (c,cty) =
     let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in
-    let combined_rels = Intset.union prev_rels direct_rels in
+    let combined_rels = Int.Set.union prev_rels direct_rels in
     let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i)))
-    in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels)))
-  in minimalrec_free_rels_rec Intset.empty
+    in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels)))
+  in minimalrec_free_rels_rec Int.Set.empty
 
 (* [sig_clausal_form siglen ty]
 
@@ -1024,7 +1024,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 let make_iterated_tuple env sigma dflt (z,zty) =
   let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in
   let sort_of_zty = get_sort_of env sigma zty in
-  let sorted_rels = Sort.list (<) (Intset.elements rels) in
+  let sorted_rels = Sort.list (<) (Int.Set.elements rels) in
   let (tuple,tuplety) =
     List.fold_left (make_tuple env sigma) (z,zty) sorted_rels
   in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a05ce2415..966309395 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2676,7 +2676,7 @@ let compute_elim_sig ?elimc elimt =
 
   let ccl = exchange_hd_app (mkVar (id_of_string "__QI_DUMMY__")) conclusion in
   let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in
-  let nparams = Intset.cardinal (free_rels concl_with_args) in
+  let nparams = Int.Set.cardinal (free_rels concl_with_args) in
   let preds,params = cut_list (List.length params_preds - nparams) params_preds in
 
   (* A first approximation, further analysis will tweak it *)
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 0c0ee38e6..20d3b2c1e 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -56,7 +56,7 @@ let rec safe_define evm ev c =
 (*  msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Pp.int ev++str" := "++pr_constr c);*)
   let evi = (Evd.find evm ev) in
   let define_subst evm sigma =
-    Util.Intmap.fold
+    Int.Map.fold
       ( fun ev (e,c) evm ->
 	  match kind_of_term c with Evar (i,_) when Int.equal i ev -> evm | _ ->
 	    safe_define evm ev (lift (-List.length e) c)
@@ -91,7 +91,7 @@ let add_gen_ctx (cl,gen,evm) ctx : signature * constr list =
    compare function for constr instead of Pervasive's one! *)
 module SubstSet : Set.S with type elt = Termops.subst
   = Set.Make (struct type t = Termops.subst
-		     let compare = Util.Intmap.compare (Pervasives.compare)
+		     let compare = Int.Map.compare (Pervasives.compare)
 	      end)
 
 (* searches instatiations in the library for just one evar [ev] of a
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 69918b2b0..c6c934a81 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -857,8 +857,8 @@ let out_def = function
   | None -> error "Program Fixpoint needs defined bodies."
 
 let collect_evars_of_term evd c ty =
-  let evars = Intset.union (evars_of_term c) (evars_of_term ty) in
-    Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
+  let evars = Int.Set.union (evars_of_term c) (evars_of_term ty) in
+    Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
       evars Evd.empty
       
 let do_program_recursive fixkind fixl ntns =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9b549084a..4abcfacf9 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -53,7 +53,7 @@ type oblinfo =
     ev_src: Evar_kinds.t Loc.located;
     ev_typ: types;
     ev_tac: tactic option;
-    ev_deps: Intset.t }
+    ev_deps: Int.Set.t }
 
 (* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
 open Store.Field
@@ -63,7 +63,7 @@ let evar_tactic = Store.field ()
   where n binders were passed through. *)
 
 let subst_evar_constr evs n idf t = 
-  let seen = ref Intset.empty in
+  let seen = ref Int.Set.empty in
   let transparent = ref Idset.empty in
   let evar_info id = List.assoc id evs in
   let rec substrec (depth, fixrels) c = match kind_of_term c with
@@ -74,7 +74,7 @@ let subst_evar_constr evs n idf t =
 	  with Not_found ->
 	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
 	in
-        seen := Intset.add id !seen;
+        seen := Int.Set.add id !seen;
 	  (* Evar arguments are created in inverse order,
 	     and we must not apply to defined ones (i.e. LetIn's)
 	  *)
@@ -125,14 +125,14 @@ let etype_of_evar evs hyps concl =
 	let t', s, trans = subst_evar_constr evs n mkVar t in
 	let t'' = subst_vars acc 0 t' in
 	let rest, s', trans' = aux (id :: acc) (succ n) tl in
-	let s' = Intset.union s s' in
+	let s' = Int.Set.union s s' in
 	let trans' = Idset.union trans trans' in
 	  (match copt with
 	      Some c -> 
 		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
 		let c' = subst_vars acc 0 c' in
 		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
-		Intset.union s'' s',
+		Int.Set.union s'' s',
 		Idset.union trans'' trans'
 	    | None ->
 		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
@@ -156,49 +156,49 @@ let rec chop_product n t =
       | _ -> None
 
 let evars_of_evar_info evi =
-  Intset.union (Evarutil.evars_of_term evi.evar_concl)
-    (Intset.union
+  Int.Set.union (Evarutil.evars_of_term evi.evar_concl)
+    (Int.Set.union
 	(match evi.evar_body with
-	| Evar_empty -> Intset.empty
+	| Evar_empty -> Int.Set.empty
 	| Evar_defined b -> Evarutil.evars_of_term b)
 	(Evarutil.evars_of_named_context (evar_filtered_context evi)))
 
 let evar_dependencies evm oev =
   let one_step deps =
-    Intset.fold (fun ev s ->
+    Int.Set.fold (fun ev s ->
       let evi = Evd.find evm ev in
       let deps' = evars_of_evar_info evi in
-	if Intset.mem oev deps' then
+	if Int.Set.mem oev deps' then
 	  raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev))
-	else Intset.union deps' s)
+	else Int.Set.union deps' s)
       deps deps
   in
   let rec aux deps =
     let deps' = one_step deps in
-      if Intset.equal deps deps' then deps
+      if Int.Set.equal deps deps' then deps
       else aux deps'
-  in aux (Intset.singleton oev)
+  in aux (Int.Set.singleton oev)
       
 let move_after (id, ev, deps as obl) l = 
   let rec aux restdeps = function
     | (id', _, _) as obl' :: tl -> 
-	let restdeps' = Intset.remove id' restdeps in
-	  if Intset.is_empty restdeps' then
+	let restdeps' = Int.Set.remove id' restdeps in
+	  if Int.Set.is_empty restdeps' then
 	    obl' :: obl :: tl
 	  else obl' :: aux restdeps' tl
     | [] -> [obl]
-  in aux (Intset.remove id deps) l
+  in aux (Int.Set.remove id deps) l
     
 let sort_dependencies evl =
   let rec aux l found list =
     match l with
     | (id, ev, deps) as obl :: tl ->
-	let found' = Intset.union found (Intset.singleton id) in
-	  if Intset.subset deps found' then
+	let found' = Int.Set.union found (Int.Set.singleton id) in
+	  if Int.Set.subset deps found' then
 	    aux tl found' (obl :: list)
 	  else aux (move_after obl tl) found list
     | [] -> List.rev list
-  in aux evl Intset.empty []
+  in aux evl Int.Set.empty []
 
 open Environ
 
@@ -292,7 +292,7 @@ let explain_no_obligations = function
 
 type obligation_info =
     (Names.identifier * Term.types * Evar_kinds.t Loc.located *
-     Evar_kinds.obligation_definition_status * Intset.t * tactic option) array
+     Evar_kinds.obligation_definition_status * Int.Set.t * tactic option) array
 
 type obligation =
   { obl_name : identifier;
@@ -300,7 +300,7 @@ type obligation =
     obl_location : Evar_kinds.t Loc.located;
     obl_body : constr option;
     obl_status : Evar_kinds.obligation_definition_status;
-    obl_deps : Intset.t;
+    obl_deps : Int.Set.t;
     obl_tac : tactic option;
   }
 
@@ -376,7 +376,7 @@ let get_obligation_body expand obl =
     else c
 
 let obl_substitution expand obls deps =
-  Intset.fold
+  Int.Set.fold
     (fun x acc ->
        let xobl = obls.(x) in
        let oblb =
@@ -494,8 +494,8 @@ let progmap_replace prg' =
   Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
 
 let rec intset_to = function
-    -1 -> Intset.empty
-  | n -> Intset.add n (intset_to (pred n))
+    -1 -> Int.Set.empty
+  | n -> Int.Set.add n (intset_to (pred n))
 
 let subst_body expand prg =
   let obls, _ = prg.prg_obligations in
@@ -605,7 +605,7 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
 	let n = Nameops.add_suffix n "_obligation" in
 	  [| { obl_name = n; obl_body = None;
 	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
-	       obl_status = Evar_kinds.Expand; obl_deps = Intset.empty;
+	       obl_status = Evar_kinds.Expand; obl_deps = Int.Set.empty;
 	       obl_tac = None } |],
 	mkVar n
     | Some b ->
@@ -686,18 +686,18 @@ let update_obls prg obls rem =
 let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
 
 let deps_remaining obls deps =
-  Intset.fold
+  Int.Set.fold
     (fun x acc ->
       if is_defined obls x then acc
       else x :: acc)
     deps []
 
 let dependencies obls n =
-  let res = ref Intset.empty in
+  let res = ref Int.Set.empty in
     Array.iteri
       (fun i obl ->
-	if not (Int.equal i n) && Intset.mem n obl.obl_deps then
-	  res := Intset.add i !res)
+	if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then
+	  res := Int.Set.add i !res)
       obls;
     !res
 
@@ -774,7 +774,7 @@ let rec solve_obligation prg num tac =
 		  match res with
 		  | Remain n when n > 0 ->
 		      let deps = dependencies obls num in
-			if not (Intset.is_empty deps) then
+			if not (Int.Set.is_empty deps) then
 			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
 		  | _ -> ());
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
@@ -830,7 +830,7 @@ and solve_prg_obligations prg ?oblset tac =
   let obls' = Array.copy obls in
   let p = match oblset with
     | None -> (fun _ -> true)
-    | Some s -> (fun i -> Intset.mem i s)
+    | Some s -> (fun i -> Int.Set.mem i s)
   in
   let _ =
     Array.iteri (fun i x ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 5dee091d3..3017db4a6 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -33,14 +33,14 @@ val check_evars : env -> evar_map -> unit
 
 val mkMetas : int -> constr list
 
-val evar_dependencies : evar_map -> int -> Intset.t
-val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * Intset.t) list
+val evar_dependencies : evar_map -> int -> Int.Set.t
+val sort_dependencies : (int * evar_info * Int.Set.t) list -> (int * evar_info * Int.Set.t) list
 
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_map -> int ->
   ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
-  (identifier * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Intset.t *
+  (identifier * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Int.Set.t *
       tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
@@ -53,7 +53,7 @@ val eterm_obligations : env -> identifier -> evar_map -> int ->
 
 type obligation_info =
   (identifier * Term.types * Evar_kinds.t Loc.located *
-      Evar_kinds.obligation_definition_status * Intset.t * tactic option) array
+      Evar_kinds.obligation_definition_status * Int.Set.t * tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)