Prise en compte des alias syntaxiques vers des references dans divers lieux de globalisation des constantes

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

2 files changed, 31 insertions, 12 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cfcbe9a917..670cc995b9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -353,9 +353,23 @@ let intern_inductive ist = function
   | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
   | r -> ArgArg (Nametab.global_inductive r)
 
+exception NotSyntacticRef
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef kn -> 
+	match Syntax_def.search_syntactic_definition loc kn with
+	  | Rawterm.RRef (_,ref) -> ref
+	  | _ -> raise NotSyntacticRef
+
 let intern_global_reference ist = function
   | Ident (loc,id) as r when find_var id ist -> ArgVar (loc,id)
-  | r -> ArgArg (loc,Nametab.global r)
+  | r -> 
+      let loc,qid = qualid_of_reference r in
+      try ArgArg (loc,locate_reference qid)
+      with _ -> 
+	error_global_not_found_loc loc qid
 
 let intern_tac_ref ist = function
   | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
@@ -377,8 +391,8 @@ let intern_constr_reference strict ist = function
   | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
       RVar (loc,id), None
   | r ->
-      let _,qid = qualid_of_reference r in
-      RRef (loc,Nametab.locate qid), if strict then None else Some (CRef r)
+      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 r =
   try Reference (intern_tac_ref ist r)
@@ -458,13 +472,7 @@ let intern_evaluable ist = function
   | r ->
       let loc,qid = qualid_of_reference r in
       try
-	let ref = match Nametab.extended_locate qid with
-	  | TrueGlobal ref -> ref
-	  | SyntacticDef kn -> 
-	      match Syntax_def.search_syntactic_definition loc kn with
-		| RRef (_,ref) -> ref
-		| _ -> error_not_evaluable (pr_reference r) in
-	let e = match ref with
+	let e = match locate_reference qid with
 	  | ConstRef c -> EvalConstRef c
 	  | VarRef c -> EvalVarRef c
 	  | _ -> error_not_evaluable (pr_reference r) in
@@ -472,7 +480,9 @@ let intern_evaluable ist = function
 	  | Ident (loc,id) when not !strict_check -> Some (loc,id)
 	  | _ -> None in
         ArgArg (e,short_name)
-      with Not_found ->
+      with
+	| NotSyntacticRef -> error_not_evaluable (pr_reference r)
+	| Not_found ->
 	match r with 
 	  | Ident (loc,id) when not !strict_check ->
 	      ArgArg (EvalVarRef id, Some (loc,id))
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5edc4eaf8a..5b84e9311f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -536,10 +536,19 @@ let vernac_import export refl =
 let vernac_canonical locqid =
   Recordobj.objdef_declare (Nametab.global locqid)
 
+let locate_reference ref =
+  let (loc,qid) = qualid_of_reference ref in
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef kn -> 
+	match Syntax_def.search_syntactic_definition loc kn with
+	  | Rawterm.RRef (_,ref) -> ref
+	  | _ -> error_global_not_found_loc loc qid
+
 let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  let ref' = Nametab.global ref in
+  let ref' = locate_reference ref in
   Class.try_add_new_coercion_with_target ref' stre source target;
   if_verbose message ((string_of_reference ref) ^ " is now a coercion")