Prise en compte des defs syntaxiques dans is_global et global_reference qui passent donc de Termops a Constrintern

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

2 files changed, 42 insertions, 0 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 53e6867057..0f68f03143 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -153,6 +153,10 @@ let set_var_scope loc id (_,scopt,scopes) (_,_,varscopes,_,_) =
     else
       idscopes := Some (scopt,scopes)
   with Not_found ->
+(*
+    if not (Options.do_translate ()) then
+      error ("Could not globalize " ^ (string_of_id id))
+*)
     if_verbose warning ("Could not globalize " ^ (string_of_id id))
 
 (**********************************************************************)
@@ -931,3 +935,33 @@ let interp_aconstr impls vars a =
   List.map
     (fun (id,r) -> (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl,
   a
+
+(**********************************************************************)
+(* Locating reference, possibly via an abbreviation *)
+
+let locate_reference qid =
+  match Nametab.extended_locate qid with
+    | TrueGlobal ref -> ref
+    | SyntacticDef kn -> 
+	match Syntax_def.search_syntactic_definition dummy_loc kn with
+	  | Rawterm.RRef (_,ref) -> ref
+	  | _ -> raise Not_found
+
+let is_global id =
+  try 
+    let _ = locate_reference (make_short_qualid id) in true
+  with Not_found -> 
+    false
+
+let global_reference id = 
+  constr_of_reference (locate_reference (make_short_qualid id))
+
+let construct_reference ctx id =
+  try
+    Term.mkVar (let _ = Sign.lookup_named id ctx in id)
+  with Not_found ->
+    global_reference id
+
+let global_reference_in_absolute_module dir id = 
+  constr_of_reference (Nametab.absolute_reference (Libnames.make_path dir id))
+
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index c1c9ede029..2b87d0d66d 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -95,6 +95,14 @@ val interp_constrpattern :
 
 val interp_reference : ltac_sign -> reference -> rawconstr
 
+(* Locating references of constructions, possibly via a syntactic definition *)
+
+val locate_reference : qualid -> global_reference
+val is_global : identifier -> bool
+val construct_reference : named_context -> identifier -> constr
+val global_reference : identifier -> constr
+val global_reference_in_absolute_module : dir_path -> identifier -> constr
+
 (* Interprets into a abbreviatable constr *)
 val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
   interpretation