diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-24 08:22:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-24 08:22:17 +0000 |
| commit | 80921b2f279b70f60cb66684f88c7e6f180f8117 (patch) | |
| tree | f65c6ea2c388e2e3c7df5f041ab4b28c9078737a | |
| parent | 16084065ebcff9eeba7231e687611fd9acb54887 (diff) | |
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
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1af19868a..a50b79720 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, |