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

10 files changed, 116 insertions, 116 deletions

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 " }"