From 80921b2f279b70f60cb66684f88c7e6f180f8117 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 24 Jul 2008 08:22:17 +0000
Subject: Propagation de l'information "strict" (càd à toplevel ou en train de
 définir une ltac) dans l'interprétation des identificateurs isolés en
 position de tactiques, comme dans "let x:=y in t" (résoud l'incompatibilité
 #1906).

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

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1af19868a3..a50b797208 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -431,7 +431,7 @@ let intern_isolated_global_tactic_reference r =
   | Ident (_,id) -> Tacexp (lookup_atomic id)
   | _ -> raise Not_found
 
-let intern_isolated_tactic_reference ist r =
+let intern_isolated_tactic_reference strict ist r =
   (* An ltac reference *)
   try Reference (intern_ltac_variable ist r)
   with Not_found ->
@@ -439,7 +439,7 @@ let intern_isolated_tactic_reference ist r =
   try intern_isolated_global_tactic_reference r
   with Not_found ->
   (* Tolerance for compatibility, allow not to use "constr:" *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference true ist r))
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
   with Not_found ->
   (* Reference not found *)
   error_global_not_found_loc (qualid_of_reference r)
@@ -899,7 +899,7 @@ and intern_tacarg strict ist = function
 	if istac then Reference (ArgVar (adjust_loc loc,id))
 	else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None))
       else error_syntactic_metavariables_not_allowed loc
-  | TacCall (loc,f,[]) -> intern_isolated_tactic_reference ist f
+  | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
   | TacCall (loc,f,l) ->
       TacCall (loc,
         intern_applied_tactic_reference ist f,
-- 
cgit v1.2.3