module Proof_trees

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

1 files changed, 18 insertions, 26 deletions

diff --git a/kernel/evd.ml b/kernel/evd.ml
index 5836f7775c..9295d35872 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -19,53 +19,45 @@ type evar_body =
   | Evar_defined of constr
 
 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 }           (* any other necessary information   *)
+  evar_concl : constr;
+  evar_hyps : typed_type signature;
+  evar_body : evar_body }
 
 type evar_map = evar_info Intmap.t
 
 let mt_evd = Intmap.empty
 
-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 to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let dom evc = Intmap.fold (fun ev _ acc -> ev::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 = 
-  Intmap.add sp newinfo evd
+let add evd ev newinfo =  Intmap.add ev newinfo evd
 
-let add_noinfo evd sp sign typ = 
-  let newinfo = 
-    { evar_concl = typ;
-      evar_hyps  = sign;
-      evar_body  = Evar_empty }
-  in 
-  Intmap.add sp newinfo evd
-
-let define evd sp body = 
-  let oldinfo = map evd sp in
+let define evd ev body = 
+  let oldinfo = map evd ev in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
-      evar_hyps  = oldinfo.evar_hyps;
-      evar_body  = Evar_defined body } 
+      evar_hyps = oldinfo.evar_hyps;
+      evar_body = Evar_defined body } 
   in
   match oldinfo.evar_body with
-    | Evar_empty -> Intmap.add sp newinfo evd
+    | Evar_empty -> Intmap.add ev newinfo evd
     | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
 
 let non_instantiated sigma = 
-  let listsp = to_list sigma in
+  let listev = to_list sigma in
   List.fold_left 
-    (fun l ((sp,evd) as d) -> 
+    (fun l ((ev,evd) as d) -> 
        if evd.evar_body = Evar_empty then (d::l) else l)
-    [] listsp
+    [] listev
     
-let is_evar sigma sp = in_dom sigma sp
+let is_evar sigma ev = in_dom sigma ev
 
-let is_defined sigma sp =
-  let info = map sigma sp in not (info.evar_body = Evar_empty)
+let is_defined sigma ev =
+  let info = map sigma ev in 
+  not (info.evar_body = Evar_empty)