From 33512e2f4d7d0733805efac1b9e69855fdf1777c Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 2 Nov 2000 15:41:00 +0000
Subject: correction Abstract (et make world passe!)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/evd.ml         | 6 ++----
 kernel/evd.mli        | 8 +++-----
 kernel/instantiate.ml | 4 ++--
 3 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'kernel')

diff --git a/kernel/evd.ml b/kernel/evd.ml
index 64602f870..548f8b14a 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -5,7 +5,6 @@ open Util
 open Names
 open Term
 open Sign
-open Environ
 
 (* The type of mappings for existential variables *)
 
@@ -21,7 +20,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_env : env;
+  evar_hyps : named_context;
   evar_body : evar_body;
   evar_info : 'a option }
 
@@ -42,7 +41,7 @@ let define evd ev body =
   let oldinfo = map evd ev in
   let newinfo =
     { evar_concl = oldinfo.evar_concl;
-      evar_env = oldinfo.evar_env;
+      evar_hyps = oldinfo.evar_hyps;
       evar_body = Evar_defined body;
       evar_info = oldinfo.evar_info } 
   in
@@ -65,7 +64,6 @@ let is_defined sigma ev =
   let info = map sigma ev in 
   not (info.evar_body = Evar_empty)
 
-let evar_hyps ev = named_context ev.evar_env
 let evar_body ev = ev.evar_body
 
 let id_of_existential ev =
diff --git a/kernel/evd.mli b/kernel/evd.mli
index e74474835..6ab60e295 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -5,13 +5,12 @@
 open Names
 open Term
 open Sign
-open Environ
 (*i*)
 
 (* The type of mappings for existential variables.
    The keys are integers and the associated information is a record
-   containing the type of the evar ([evar_concl]), the environment under which 
-   it was introduced ([evar_env]) and its definition ([evar_body]). 
+   containing the type of the evar ([evar_concl]), the context under which 
+   it was introduced ([evar_hyps]) and its definition ([evar_body]). 
    [evar_info] is used to add any other kind of information. *)
 
 type evar = int
@@ -24,7 +23,7 @@ type evar_body =
 
 type 'a evar_info = {
   evar_concl : constr;
-  evar_env : env;
+  evar_hyps : named_context;
   evar_body : evar_body;
   evar_info : 'a option }
 
@@ -48,7 +47,6 @@ val is_evar : 'a evar_map -> evar -> bool
 
 val is_defined : 'a evar_map -> evar -> bool
 
-val evar_hyps : 'a evar_info -> named_context
 val evar_body : 'a evar_info -> evar_body
 
 val id_of_existential : evar -> identifier
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index e433423c0..f99ccb0c4 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -61,7 +61,7 @@ let name_of_existential n = id_of_string ("?" ^ string_of_int n)
 
 let existential_type sigma (n,args) =
   let info = Evd.map sigma n in
-  let hyps = evar_hyps info in
+  let hyps = info.evar_hyps in
   (* TODO: check args [this comment was in Typeops] *)
   instantiate_constr hyps info.evar_concl (Array.to_list args)
 
@@ -69,7 +69,7 @@ exception NotInstantiatedEvar
 
 let existential_value sigma (n,args) =
   let info = Evd.map sigma n in
-  let hyps = evar_hyps info in
+  let hyps = info.evar_hyps in
   match evar_body info with
     | Evar_defined c ->
 	instantiate_constr hyps c (Array.to_list args)
-- 
cgit v1.2.3