diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-10 08:19:50 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-10 08:19:50 +0000 |
| commit | c72121404b3effcb48ddf25063fd6b3fe6573319 (patch) | |
| tree | cebf05927f84e352d163293ab4522652e075f78b /tactics | |
| parent | 64b34d88034bf778cc8f4b845a11f5faacc3de3e (diff) | |
Trop de restriction pour les TacDef
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3899 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0be8ccec6..ca8f5485d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -383,7 +383,7 @@ let intern_tactic_reference ist r = error_global_not_found_loc loc qid let intern_constr_reference strict ist = function - | Ident (_,id) when find_hyp id ist or (not strict & find_ctxvar id ist) -> + | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist -> RVar (loc,id), None | r -> let _,qid = qualid_of_reference r in @@ -452,7 +452,7 @@ let intern_evaluable_or_metanum ist = function ArgArg (EvalVarRef id, Some id) | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id) | r -> - let e = match fst (intern_constr_reference true ist r) with + let e = match fst(intern_constr_reference !strict_check ist r) with | RRef (_,ConstRef c) -> EvalConstRef c | RRef (_,VarRef c) | RVar (_,c) -> EvalVarRef c | _ -> error_not_evaluable (pr_reference r) in |