From 4116276142fd33901239def9d45fe41ffbcb248b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Dec 2000 10:55:31 +0000
Subject: Déplacement du type stack de Reduction vers Closure et utilisation
 pour accélérer la réduction dans Closure

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1221 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 1 +
 pretyping/tacred.ml   | 3 +--
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index c90dcddb13..f0b50aa0d2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -5,6 +5,7 @@ open Util
 open Names
 open Term
 open Reduction
+open Closure
 open Instantiate
 open Environ
 open Typing
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 1e162a4bdb..715cb798a0 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -8,6 +8,7 @@ open Term
 open Inductive
 open Environ
 open Reduction
+open Closure
 open Instantiate
 
 (************************************************************************)
@@ -582,8 +583,6 @@ let rec substlin env name n ol c =
     | (IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _
       |IsEvar _|IsConst _|IsMutInd _|IsMutConstruct _) -> (n,ol,c)
 	
-open Closure
-	  
 let unfold env sigma name =
   clos_norm_flags (unfold_flags name) env sigma
 
-- 
cgit v1.2.3