From 4eee15dcf54e665f38f5b85f7b3a7f9dcded7e07 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Oct 2000 14:21:38 +0000
Subject: C'était pas le bon env dans build_term

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@689 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/wcclausenv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index de5adc94df..320e8d56f3 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -128,7 +128,7 @@ let rec build_args acc ce p_0 p_1 =
     | (_, (_::_)) -> failwith "mk_clenv_using"
 
 and build_term ce p_0 c =
-  let env = Global.env() in
+  let env = w_env ce.hook in
   match p_0, kind_of_term c with 
     | ((na,Some t), IsMeta mv) -> 
 (*    	let mv = new_meta() in *)
-- 
cgit v1.2.3