From 33512e2f4d7d0733805efac1b9e69855fdf1777c Mon Sep 17 00:00:00 2001
From: filliatr
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 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'kernel/evd.ml')

diff --git a/kernel/evd.ml b/kernel/evd.ml
index 64602f870c..548f8b14ac 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 =
-- 
cgit v1.2.3