From f50ae4202023257791cd28e1e0e5098fa1ce9290 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Sep 2003 09:51:06 +0000
Subject: Bug internalisation des Extern: la globalisation doit etre stricte

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

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 536ddfb66c..619d26c619 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2056,7 +2056,9 @@ let _ = Auto.set_extern_interp
     let l = List.map (fun (id,c) -> (id,VConstr c)) l in
     interp_tactic {lfun=l;debug=get_debug()})
 let _ = Auto.set_extern_intern_tac 
-  (fun l -> intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})
+  (fun l ->
+    Options.with_option strict_check
+    (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
 let _ = Auto.set_extern_subst_tactic subst_tactic
 let _ = Dhyp.set_extern_interp eval_tactic
 let _ = Dhyp.set_extern_intern_tac
-- 
cgit v1.2.3