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

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 ->