redeplacement des var. ex. dans kernel :-)

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

3 files changed, 4 insertions, 118 deletions

diff --git a/proofs/evd.ml b/proofs/evd.ml
deleted file mode 100644
index 48b2a4b577..0000000000
--- a/proofs/evd.ml
+++ /dev/null
@@ -1,68 +0,0 @@
-
-(* $Id$ *)
-
-open Util
-open Names
-open Term
-open Sign
-
-(* The type of mappings for existential variables *)
-
-type evar_body =
-  | Evar_empty 
-  | Evar_defined of constr
-
-type 'a 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   *)
-
-type 'a evar_map = 'a evar_info Spmap.t
-
-let mt_evd = Spmap.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 add_with_info evd sp newinfo = 
-  Spmap.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}
-  in 
-  Spmap.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} 
-  in
-  match oldinfo.evar_body with
-    | Evar_empty -> Spmap.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
-  List.fold_left 
-    (fun l ((sp,evd) as d) -> 
-       if evd.evar_body = Evar_empty then (d::l) else l)
-    [] listsp
-    
-let is_evar sigma sp = in_dom sigma sp
-
-let is_defined sigma sp =
-  let info = map sigma sp in not (info.evar_body = Evar_empty)
diff --git a/proofs/evd.mli b/proofs/evd.mli
deleted file mode 100644
index 8063f42b02..0000000000
--- a/proofs/evd.mli
+++ /dev/null
@@ -1,48 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Term
-open Sign
-(*i*)
-
-(* The type of mappings for existential variables.
-   The keys are section paths and the associated information is a record
-   containing the type of the evar ([concl]), the signature under which 
-   it was introduced ([hyps]), its definition ([body]) and any other 
-   possible information if necessary ([info]).
-*)
-
-type evar_body =
-  | Evar_empty 
-  | Evar_defined of constr
-
-type 'a evar_info = {
-  evar_concl : typed_type;
-  evar_hyps  : typed_type signature;
-  evar_body  : evar_body;
-  evar_info  : 'a option }
-
-type 'a evar_map
-
-val dom    : 'a evar_map -> section_path list
-val map    : 'a evar_map -> section_path -> 'a evar_info
-val rmv    : 'a evar_map -> section_path -> 'a evar_map
-val remap  : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val in_dom : 'a evar_map -> section_path -> bool
-val toList : 'a evar_map -> (section_path * 'a evar_info) list
-
-val mt_evd : 'a evar_map
-val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map
-val add_noinfo : 
-  'a evar_map -> section_path -> typed_type signature -> typed_type 
-    -> 'a evar_map
-
-val define : 'a evar_map -> section_path -> constr -> 'a evar_map
-
-val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
-val is_evar : 'a evar_map -> section_path -> bool
-
-val is_defined : 'a evar_map -> section_path -> bool
-
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 0366cd25b2..ce5dfbc607 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -3,6 +3,8 @@
 
 (*i*)
 open Pp
+open Term
+open Sign
 open Proof_trees
 (*i*)
 
@@ -11,7 +13,7 @@ val pr_prim_rule : prim_rule -> std_ppcmds
 val prim_refiner : prim_rule -> 'a Evd.evar_map -> goal -> goal list
 
 val prim_extractor : 
-  ((type_judgement, constr) env -> proof_tree -> constr) -> 
-    (type_judgement, constr) env -> proof_tree -> constr
+  ((typed_type, constr) env -> proof_tree -> constr) -> 
+    (typed_type, constr) env -> proof_tree -> constr
 
 val extract_constr : constr assumptions -> constr -> constr