On passe les last_mods (un des champs de Evd.evar_defs) de list

d'entiers à ensemble d'entier. A première vue l'optimisation a un effet
négligeable.
Mais vu l'utilisation qui est fait des des last_mods (des mem à
répétition). C'est plus raisonnable ainsi.


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

3 files changed, 13 insertions, 10 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0ef2c63191..29b5b87a7d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1094,9 +1094,9 @@ let solve_pattern_eqn env l1 c =
 
 let status_changed lev (pbty,_,t1,t2) =
   try 
-    List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
+    ExistentialSet.mem (head_evar t1) lev or ExistentialSet.mem (head_evar t2) lev
   with Failure _ ->
-    try List.mem (head_evar t2) lev with Failure _ -> false
+    try ExistentialSet.mem (head_evar t2) lev with Failure _ -> false
 
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
  * definitions. We try to unify the xi with the yi pairwise. The pairs
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fd12ad3998..6bc77abcb6 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -71,6 +71,7 @@ let eq_evar_info ei1 ei2 =
 *)
 
 module ExistentialMap = Intmap
+module ExistentialSet = Intset
 
 (* This exception is raised by *.existential_value *)	
 exception NotInstantiatedEvar
@@ -423,7 +424,7 @@ type evar_constraint = conv_pb * Environ.env * constr * constr
 type evar_defs =
     { evars : EvarMap.t;
       conv_pbs : evar_constraint list;
-      last_mods : existential_key list;
+      last_mods : ExistentialSet.t;
       history : (existential_key * (loc * hole_kind)) list;
       metas : clbinding Metamap.t }
 
@@ -440,7 +441,7 @@ let merge d1 d2 = {
 (* d1 with evars = EvarMap.merge d1.evars d2.evars*)
   evars = EvarMap.merge d1.evars d2.evars ;
   conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ;
-  last_mods = List.rev_append d1.last_mods d2.last_mods ;
+  last_mods = ExistentialSet.union d1.last_mods d2.last_mods ;
   history = List.rev_append d1.history d2.history ;
   metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas
 }
@@ -492,14 +493,14 @@ let subst_evar_map = subst_evar_defs_light
 
 (* spiwack: deprecated *)
 let create_evar_defs sigma = { sigma with
-  conv_pbs=[]; last_mods=[]; history=[]; metas=Metamap.empty }
+  conv_pbs=[]; last_mods=ExistentialSet.empty; history=[]; metas=Metamap.empty }
 (* spiwack: tentatively deprecated *)
 let create_goal_evar_defs sigma = { sigma with
-   conv_pbs=[]; last_mods=[]; metas=Metamap.empty }
+   conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty }
 let empty =  { 
   evars=EvarMap.empty; 
   conv_pbs=[]; 
-  last_mods = []; 
+  last_mods = ExistentialSet.empty; 
   history=[]; 
   metas=Metamap.empty 
 }
@@ -517,7 +518,7 @@ let define evk body evd =
     last_mods = 
         match evd.conv_pbs with
 	| [] ->  evd.last_mods
-        | _ -> evk :: evd.last_mods }
+        | _ -> ExistentialSet.add evk evd.last_mods }
 
 let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
   let filter =
@@ -565,7 +566,7 @@ let extract_conv_pbs evd p =
       ([],[])
       evd.conv_pbs
   in
-  {evd with conv_pbs = pbs1; last_mods = []},
+  {evd with conv_pbs = pbs1; last_mods = ExistentialSet.empty},
   pbs
 
 let extract_changed_conv_pbs evd p =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 8ea0227fed..ac708d1ec7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -195,8 +195,10 @@ val evar_merge : evar_defs -> evar_defs -> evar_defs
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_defs -> evar_defs
+
+module ExistentialSet : Set.S with type elt = existential_key
 val extract_changed_conv_pbs : evar_defs -> 
-      (existential_key list -> evar_constraint -> bool) ->
+      (ExistentialSet.t -> evar_constraint -> bool) ->
       evar_defs * evar_constraint list
 val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list