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

9 files changed, 47 insertions, 24 deletions

diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml
index 46d86a3f6b..28327ee27e 100644
--- a/contrib/correctness/pdb.ml
+++ b/contrib/correctness/pdb.ml
@@ -14,6 +14,7 @@ open Names
 open Term
 open Termops
 open Nametab
+open Constrintern
 
 open Ptype
 open Past
diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml
index 18498377fb..3d802c4e70 100644
--- a/contrib/correctness/perror.ml
+++ b/contrib/correctness/perror.ml
@@ -66,7 +66,7 @@ let check_for_array loc id = function
 let is_constant_type s = function
     TypePure c ->
       let id = id_of_string s in
-      let c' = Termops.global_reference id in
+      let c' = Constrintern.global_reference id in
       Reductionops.is_conv (Global.env()) Evd.empty c c'
   | _ -> false 
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index ba96b98b71..5fbcf4489f 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -170,7 +170,7 @@ let coq_false = mkConstruct ((bool_sp,0),2)
 
 let constant s =
   let id = Constrextern.id_of_v7_string s in
-  Termops.global_reference id
+  Constrintern.global_reference id
 
 let connective_and = id_of_string "prog_bool_and"
 let connective_or  = id_of_string "prog_bool_or"
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
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 23f9a7ffc7..f9e949c84c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -899,17 +899,3 @@ let rec rename_bound_var env l c =
   | Cast (c,t) -> mkCast (rename_bound_var env l c, t)
   | x -> c
 
-(* References to constr *)
-
-let global_reference id = 
-  constr_of_reference (Nametab.locate (make_short_qualid id))
-
-let construct_reference ctx id =
-  try
-    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/pretyping/termops.mli b/pretyping/termops.mli
index af75cfd2d1..da3033b0c0 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -181,12 +181,5 @@ val make_all_name_different : env -> env
 val global_vars : env -> constr -> identifier list
 val global_vars_set_of_decl : env -> named_declaration -> Idset.t
 
-(* References to constr *)
-
-val construct_reference : named_context -> identifier -> constr
-val global_reference : identifier -> constr
-val global_reference_in_absolute_module : dir_path -> identifier -> constr
-
 (* Test if an identifier is the basename of a global reference *)
-val is_global : identifier -> bool
 val is_section_variable : identifier -> bool
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 32951721b5..d6e2245306 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -87,7 +87,7 @@ let pf_interp_type gls c =
   let evc = project gls in 
   Constrintern.interp_type evc (pf_env gls) c
 
-let pf_global gls id = construct_reference (pf_hyps gls) id
+let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
 
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 6d5fe1a801..bc093cf5de 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -28,6 +28,7 @@ open Vernacexpr
 open Safe_typing
 open Nametab
 open Decl_kinds
+open Constrintern
 
 type setoid =
     { set_a : constr;