- re-introduction d'une evar_map dans unsafe_env

 - les var. ex. sont des entiers, et non plus des section_path


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

1 files changed, 22 insertions, 19 deletions

diff --git a/kernel/evd.ml b/kernel/evd.ml
index 48b2a4b57..5836f7775 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -8,55 +8,58 @@ open Sign
 
 (* The type of mappings for existential variables *)
 
+type evar = int
+
+let new_evar =
+  let evar_ctr = ref 0 in
+  fun () -> incr evar_ctr; !evar_ctr
+
 type evar_body =
   | Evar_empty 
   | Evar_defined of constr
 
-type 'a evar_info = {
+type evar_info = {
   evar_concl : typed_type;           (* the type of the evar ...          *)
   evar_hyps  : typed_type signature; (* ... under a certain signature     *)
-  evar_body  : evar_body;            (* its definition                    *) 
-  evar_info  : 'a option }           (* any other necessary information   *)
+  evar_body  : evar_body }           (* any other necessary information   *)
 
-type 'a evar_map = 'a evar_info Spmap.t
+type evar_map = evar_info Intmap.t
 
-let mt_evd = Spmap.empty
+let mt_evd = Intmap.empty
 
-let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc []
-let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc []
-let map evc k = Spmap.find k evc
-let rmv evc k = Spmap.remove k evc
-let remap evc k i = Spmap.add k i evc
-let in_dom evc k = Spmap.mem k evc
+let to_list evc = Intmap.fold (fun sp x acc -> (sp,x)::acc) evc []
+let dom evc = Intmap.fold (fun sp _ acc -> sp::acc) evc []
+let map evc k = Intmap.find k evc
+let rmv evc k = Intmap.remove k evc
+let remap evc k i = Intmap.add k i evc
+let in_dom evc k = Intmap.mem k evc
 
 let add_with_info evd sp newinfo = 
-  Spmap.add sp newinfo evd
+  Intmap.add sp newinfo evd
 
 let add_noinfo evd sp sign typ = 
   let newinfo = 
     { evar_concl = typ;
       evar_hyps  = sign;
-      evar_body  = Evar_empty;
-      evar_info  = None}
+      evar_body  = Evar_empty }
   in 
-  Spmap.add sp newinfo evd
+  Intmap.add sp newinfo evd
 
 let define evd sp body = 
   let oldinfo = map evd sp in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
       evar_hyps  = oldinfo.evar_hyps;
-      evar_body  = Evar_defined body;
-      evar_info  = oldinfo.evar_info} 
+      evar_body  = Evar_defined body } 
   in
   match oldinfo.evar_body with
-    | Evar_empty -> Spmap.add sp newinfo evd
+    | Evar_empty -> Intmap.add sp newinfo evd
     | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
 
 let non_instantiated sigma = 
-  let listsp = toList sigma in
+  let listsp = to_list sigma in
   List.fold_left 
     (fun l ((sp,evd) as d) -> 
        if evd.evar_body = Evar_empty then (d::l) else l)