diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/tacinterp.ml | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4ce3fcc04..e284554e7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -443,20 +443,18 @@ let intern_constr_reference strict ist = function let loc,qid = qualid_of_reference r in RRef (loc,locate_reference qid), if strict then None else Some (CRef r) -let intern_reference strict ist = function - | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id) - | r -> - (try Reference (intern_tac_ref ist r) +let intern_reference strict ist r = + (try Reference (intern_tac_ref ist r) + with Not_found -> + (try + ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> - (try - ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) - with Not_found -> - (match r with - | Ident (loc,id) when not strict -> - IntroPattern (IntroIdentifier id) - | _ -> - let (loc,qid) = qualid_of_reference r in - error_global_not_found_loc loc qid))) + (match r with + | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id) + | Ident (loc,id) when not strict -> IntroPattern (IntroIdentifier id) + | _ -> + let (loc,qid) = qualid_of_reference r in + error_global_not_found_loc loc qid))) let rec intern_intro_pattern lf ist = function | IntroOrAndPattern l -> |