Relachement globalisation Unfold en usage interactif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 29 insertions, 18 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 0f2e031cc7..e1df0ab721 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -40,7 +40,7 @@ type argument_type =
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a or_metanum = AN of 'a | MetaNum of int located
-type 'a and_short_name = 'a * identifier option
+type 'a and_short_name = 'a * identifier located option
 type rawconstr_and_expr = rawconstr * constr_expr option
 
 (* Dynamics but tagged by a type expression *)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index c938d4c516..88865f022a 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -17,7 +17,7 @@ open Topconstr
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a or_metanum = AN of 'a | MetaNum of int located
-type 'a and_short_name = 'a * identifier option
+type 'a and_short_name = 'a * identifier located option
 
 (* In globalize tactics, we need to keep the initial constr_expr to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ca8f5485db..efeacafe81 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -446,20 +446,28 @@ let intern_induction_arg ist = function
 
 (* Globalizes a reduction expression *)
 let intern_evaluable_or_metanum ist = function
-  | AN qid ->
-      let e = match qid with
-        | Ident (loc,id) when find_ctxvar id ist ->
-            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 !strict_check ist r) with
-            | RRef (_,ConstRef c) -> EvalConstRef c
-            | RRef (_,VarRef c) | RVar (_,c) -> EvalVarRef c
-            | _ -> error_not_evaluable (pr_reference r) in
-            let short_name = match r with
-              | Ident (_,id) when not !strict_check -> Some id
-              | _ -> None in
-            ArgArg (e,short_name) 
+  | AN r ->
+      let e = match r with
+        | Ident (loc,id) as r when find_ltacvar id ist -> ArgVar (loc,id)
+	| Ident (_,id) when
+	    (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
+	    ArgArg (EvalVarRef id, None)
+	| r ->
+	    let _,qid = qualid_of_reference r in
+	    try
+	      let e = match Nametab.locate qid with
+		| ConstRef c -> EvalConstRef c
+		| VarRef c -> EvalVarRef c
+		| _ -> error_not_evaluable (pr_reference r) in
+              let short_name = match r with
+		| Ident (loc,id) when not !strict_check -> Some (loc,id)
+		| _ -> None in
+              ArgArg (e,short_name)
+	    with Not_found ->
+	      match r with 
+		| Ident (loc,id) when not !strict_check ->
+		    ArgArg (EvalVarRef id, Some (loc,id))
+		| _ -> error_global_not_found_loc loc qid
       in AN e
   | MetaNum (_loc,n) -> MetaNum (loc,intern_metanum ist loc n)
 
@@ -1060,12 +1068,15 @@ let interp_evaluable_or_metanum ist env = function
   | MetaNum (loc,n) ->
       coerce_to_evaluable_ref env (VConstr (List.assoc n ist.lmatch))
   | AN r -> match r with
-      | ArgArg (r,Some id) ->
+      | ArgArg (r,Some (loc,id)) ->
           (* Maybe [id] has been introduced by Intro-like tactics *)
           (try match Environ.lookup_named id env with
             | (_,Some _,_) -> EvalVarRef id
             | _ -> error_not_evaluable (pr_id id)
-          with Not_found -> r)
+          with Not_found ->
+	    match r with
+	      | EvalConstRef _ -> r
+	      | _ -> Pretype_errors.error_var_not_found_loc loc id)
       | ArgArg (r,None) -> r
       | ArgVar (_,id) -> 
           coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))