Actually using the domain function for maps.

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

7 files changed, 10 insertions, 14 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4ab85e0e6c..363f43fd75 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -358,11 +358,9 @@ let locate_if_isevar loc na = function
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
-  { env with impls = Id.Map.fold (fun id x ->
-       let x = match x with
+  { env with impls = Id.Map.map (function
          | (Inductive _,b,c,d) -> (Inductive [],b,c,d)
-         | x -> x
-       in Id.Map.add id x) env.impls Id.Map.empty }
+         | x -> x) env.impls }
 
 let check_hidden_implicit_parameters id impls =
   if Id.Map.exists (fun _ -> function
diff --git a/interp/notation.ml b/interp/notation.ml
index a5a6138f6e..624fa23aa0 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -771,7 +771,7 @@ let pr_notation_info prglob ntn c =
 
 let pr_named_scope prglob scope sc =
  (if String.equal scope default_scope then
-   match String.Map.fold (fun _ _ x -> x+1) sc.notations 0 with
+   match String.Map.cardinal sc.notations with
      | 0 -> str "No lonely notation"
      | n -> str "Lonely notation" ++ (if Int.equal n 1 then mt() else str"s")
   else
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 60c4e88bc3..f52694edf0 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -429,7 +429,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 	       in the type of ev and adjust the source of the dependency *)
 	    let nconcl =
 	      try
-                let nids = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) rids Id.Set.empty in
+                let nids = Id.Map.domain rids in
                 check_and_clear_in_constr evdref (EvarTypingBreak ev) nids (evar_concl evi)
 	      with ClearDependencyError (rid,err) ->
 		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 3b4aa094f9..35c0b73e3a 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -146,7 +146,7 @@ module EvarInfoMap = struct
   let fold_undefined (def,undef) f a =
     ExistentialMap.fold f undef a
   let exists_undefined (def,undef) f =
-    ExistentialMap.fold (fun k v b -> b || f k v) undef false
+    ExistentialMap.exists f undef
 
   let add (def,undef) evk newinfo = match newinfo.evar_body with
   | Evar_empty -> (def, ExistentialMap.add evk newinfo undef)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9046be4d27..e917494315 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -432,7 +432,7 @@ let instances r =
   let cl = class_info r in instances_of cl    
 
 let is_class gr = 
-  Refmap.fold (fun k v acc -> acc || eq_gr v.cl_impl gr) !classes false
+  Refmap.exists (fun _ v -> eq_gr v.cl_impl gr) !classes
 
 let is_instance = function
   | ConstRef c ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71312259ed..63d77af662 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -509,9 +509,8 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
        context at globalization time: we retype with the now known
        intros/lettac/inversion hypothesis names *)
   | Some c ->
-      let fold id _ accu = Id.Set.add id accu in
-      let ltacvars = Id.Map.fold fold constrvars Id.Set.empty in
-      let bndvars = Id.Map.fold fold ist.lfun Id.Set.empty in
+      let ltacvars = Id.Map.domain constrvars in
+      let bndvars = Id.Map.domain ist.lfun in
       let ltacdata = (ltacvars, bndvars) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
@@ -1961,8 +1960,7 @@ let interp_tac_gen lfun avoid_ids debug t gl =
   let extra = TacStore.set TacStore.empty f_debug debug in
   let extra = TacStore.set extra f_avoid_ids avoid_ids in
   let ist = { lfun = lfun; extra = extra } in
-  let fold x _ accu = Id.Set.add x accu in
-  let ltacvars = Id.Map.fold fold lfun Id.Set.empty in
+  let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
     (intern_pure_tactic {
       ltacvars; ltacrecvars = Id.Map.empty;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b0f150158d..a6826b9db9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2447,7 +2447,7 @@ let hyps_of_vars env sign nogen hyps =
 	  else if Id.Set.mem x hs then (hs,x::hl)
 	  else
 	    let xvars = global_vars_set_of_decl env d in
-	      if not (Id.Set.equal (Id.Set.diff xvars hs) Id.Set.empty) then
+	      if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then
 		(Id.Set.add x hs, x :: hl)
 	      else (hs, hl))
         ~init:(hyps,[])