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

4 files changed, 15 insertions, 15 deletions

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 *)