Small code cleaning in Evarutil.

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

1 files changed, 17 insertions, 15 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index dec5e811ca..920fb54180 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -165,34 +165,36 @@ let new_meta =
 
 let mk_new_meta () = mkMeta(new_meta())
 
+(** Transfer an evar from [sigma2] to [sigma1] *)
+let transfer ev (sigma1, sigma2) =
+  let nsigma1 = Evd.add sigma1 ev (Evd.find sigma2 ev) in
+  let nsigma2 = Evd.remove sigma2 ev in
+  (nsigma1, nsigma2)
+
 let collect_evars emap c =
   let rec collrec acc c =
     match kind_of_term c with
       | Evar (evk,_) ->
-	  if Evd.is_undefined emap evk then evk::acc
+	  if Evd.is_undefined emap evk then Evar.Set.add evk acc
 	  else (* No recursion on the evar instantiation *) acc
       | _         ->
 	  fold_constr collrec acc c in
-  List.uniquize (collrec [] c)
+  collrec Evar.Set.empty c
 
 let push_dependent_evars sigma emap =
-  Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') ->
-    List.fold_left
-      (fun (sigma',emap') ev ->
-	(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
-      (sigma',emap') (collect_evars emap' ccl))
-    emap (sigma,emap)
+  let fold ev {evar_concl = ccl} (sigma, emap) =
+    Evar.Set.fold transfer (collect_evars emap ccl) (sigma, emap)
+  in
+  Evd.fold_undefined fold emap (sigma, emap)
 
 let push_duplicated_evars sigma emap c =
-  let rec collrec (one,(sigma,emap) as acc) c =
+  let rec collrec (one, evars as acc) c =
     match kind_of_term c with
-    | Evar (evk,_) when not (Evd.mem sigma evk) ->
-	if List.mem evk one then
-	  let sigma' = Evd.add sigma evk (Evd.find emap evk) in
-	  let emap' = Evd.remove emap evk in
-	  (one,(sigma',emap'))
+    | Evar (evk,_) when not (Evd.mem (fst evars) evk) ->
+	if List.exists (fun ev -> Evar.equal evk ev) one then
+	  (one, transfer evk evars)
 	else
-	  (evk::one,(sigma,emap))
+	  (evk::one, evars)
     | _ ->
 	fold_constr collrec acc c
   in