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

11 files changed, 84 insertions, 84 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ab9ed29935..c02dbba23d 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 5303252c84..3cf0c50ba2 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 4996f86c24..b82f18da73 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 a4f9ff486b..fb53654de3 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 8849f17699..8722516bbf 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 a456d08cce..9f4badd220 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 8e4351deb0..c7819e1344 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 fc78b0dcad..6c2f8f1898 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 973f85818c..4a267dd7e6 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 4d9ce49690..096cdbcbb3 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 bf0f47a32c..facc243e21 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 ->