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

3 files changed, 8 insertions, 8 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f431e04d83..c129306d27 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 0dceecf4f1..2fdf62d264 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 6a7a588d48..22da1a9662 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)