From 3c87bc951eed7bf2b6362af329b1e3a939ac26fe Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 29 Apr 2005 18:07:39 +0000 Subject: Improved order of interpretation of atomic tactics (cf bug #952) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6972 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacinterp.ml | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) (limited to 'tactics') 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 -> -- cgit v1.2.3