From 2b4201841c437ef86659eda7e1d1555eea39e626 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 16 Jul 2002 09:28:43 +0000
Subject: Bug dans la globalisation des arguments de tactiques primitives

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2882 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1bebcec498..d3721d0157 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -895,19 +895,21 @@ let hyp_or_metanum_interp ist = function
 let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
 
 let interp_pure_qualid ist (loc,qid) =
+  try VConstr (constr_of_reference (find_reference ist qid))
+  with Not_found ->
+    let (dir,id) = repr_qualid qid in
+    if dir = empty_dirpath then VIdentifier id
+    else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference")
+
+let interp_ltac_qualid ist (loc,qid as lqid) =
   try (!forward_vcontext_interp ist (lookup qid))
-  with | Not_found ->
-    try VConstr (constr_of_reference (find_reference ist qid))
-    with Not_found ->
-      let (dir,id) = repr_qualid qid in
-      if dir = empty_dirpath then VIdentifier id
-      else user_err_loc (loc,"interp_pure_qualid",str "Unknown reference")
+  with Not_found -> interp_pure_qualid ist lqid
 
 let interp_ltac_reference ist = function
   | RIdent (loc,id) -> 
       (try unrec (List.assoc id ist.lfun)
-      with | Not_found -> interp_pure_qualid ist (loc,make_short_qualid id))
-  | RQualid qid -> interp_pure_qualid ist qid
+      with | Not_found -> interp_ltac_qualid ist (loc,make_short_qualid id))
+  | RQualid qid -> interp_ltac_qualid ist qid
 
 (* Interprets a qualified name *)
 let eval_qualid ist (loc,qid as locqid) =
-- 
cgit v1.2.3