From 8e1e1503a1736dc7b5ab1a0d34dbc2e3e451998e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 22 Jan 2003 20:55:50 +0000
Subject: Mauvais environnement d'évaluation pour les globaux

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

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b3656c419f..fdafe9a64d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1107,7 +1107,7 @@ and eval_tactic ist = function
   | TacArg a -> assert false
 
 and interp_ltac_qualid is_applied ist gl (loc,qid as lqid) =
-  try val_interp ist gl (lookup qid)
+  try val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid)
   with Not_found -> interp_pure_qualid is_applied (pf_env gl) lqid
 
 and interp_ltac_reference isapplied ist gl = function
-- 
cgit v1.2.3