From 6e34881bf892602f297797481880ffa1d7db139d Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 25 Aug 2013 22:34:15 +0000
Subject: 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
---
 tactics/tacinterp.ml | 8 +++-----
 tactics/tactics.ml   | 2 +-
 2 files changed, 4 insertions(+), 6 deletions(-)

(limited to 'tactics')

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,[])
-- 
cgit v1.2.3