From fd28f10096f82ef133bbf10512c8bee617b6b8b3 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 8 Oct 1999 08:18:57 +0000
Subject: deplacements des var. ex. hors du noyau

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.mli | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'kernel/closure.mli')

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 62caafe557..ea7defa201 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,6 @@ open Pp
 open Names
 open Generic
 open Term
-open Evd
 open Environ
 (*i*)
 
@@ -83,7 +82,7 @@ val fixp_reducible :
 
 (* normalization of a constr: the two functions to know... *)
 type 'a cbv_infos
-val create_cbv_infos : flags -> 'a unsafe_env -> 'a cbv_infos
+val create_cbv_infos : flags -> unsafe_env -> 'a cbv_infos
 val cbv_norm : 'a cbv_infos -> constr -> constr
 
 (* recursive functions... *)
@@ -159,8 +158,8 @@ type case_status =
 
 (* Constant cache *)
 type 'a clos_infos
-val create_clos_infos : flags -> 'a unsafe_env -> 'a clos_infos
-val clos_infos_env : 'a clos_infos -> 'a unsafe_env
+val create_clos_infos : flags -> unsafe_env -> 'a clos_infos
+val clos_infos_env : 'a clos_infos -> unsafe_env
 
 (* Reduction function *)
 val norm_val : 'a clos_infos -> fconstr -> constr
-- 
cgit v1.2.3