- global_reference traite des variables

 - construct_reference, avec environnement en argument
 - link de Class
 - Definition et Check au toplevel


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

2 files changed, 30 insertions, 14 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ed63983f71..91fcc7df6c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -218,19 +218,26 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let global_operator sp id =
+let construct_operator env sp id =
   try
-    let cb = Global.lookup_constant sp in Const sp, cb.const_hyps
+    let cb = Environ.lookup_constant sp env in Const sp, cb.const_hyps
   with Not_found -> 
-    let mib = Global.lookup_mind sp in
+    let mib = Environ.lookup_mind sp env in
     mind_oper_of_id sp id mib, mib.mind_hyps
 
-let global_reference kind id =
+let global_operator sp id = construct_operator (Global.env()) sp id
+
+let construct_reference env kind id =
   let sp = Nametab.sp_of_id kind id in
-  let (oper,_) = global_operator sp id in
-  let hyps = Global.var_context () in
-  let ids = ids_of_sign hyps in
-  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+  try
+    let (oper,_) = construct_operator env sp id in
+    let hyps = Global.var_context () in
+    let ids = ids_of_sign hyps in
+    DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+  with Not_found -> 
+    VAR (let _ = Environ.lookup_var id env in id)
+
+let global_reference kind id = construct_reference (Global.env()) kind id
 
 let global_reference_imps kind id =
   let c = global_reference kind id in
@@ -241,6 +248,8 @@ let global_reference_imps kind id =
 	c, list_of_implicits (inductive_implicits (sp,i))
     | DOPN (MutConstruct ((sp,i),j),_) ->
 	c, list_of_implicits (constructor_implicits ((sp,i),j))
+    | VAR id ->
+	c, implicits_of_var kind id
     | _ -> assert false
 
 let global env id =
diff --git a/library/declare.mli b/library/declare.mli
index 11f6b24979..4fe7767fd6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -47,17 +47,24 @@ val out_variable : section_path -> identifier * typed_type * strength * bool
 val variable_strength : identifier -> strength
 
 
-(*s It also provides a function [global_reference] to construct a global
-  constr (a constant, an inductive or a constructor) from an identifier.
-  To do so, it first looks for the section path using [Nametab.sp_of_id] and
-  then constructs the corresponding term, associated to the current 
-  environment of variables. *)
+(*s [global_operator sp id] returns the operator (constant, inductive or
+    construtor) corresponding to [(sp,id)] in global environment, together
+    with its definition environment. *)
 
 val global_operator : section_path -> identifier -> sorts oper * var_context
+
+(*s [global_reference k id] returns the object corresponding to
+    the name [id] in the global environment. It may be a constant, 
+    an inductive, a construtor or a variable. It is instanciated
+    on the current environment of variables. [Nametab.sp_of_id] is used
+    to find the corresponding object. 
+    [construct_reference] is a version which looks for variables in a 
+    given environment instead of looking in the current global environment. *)
+
 val global_reference : path_kind -> identifier -> constr
 val global_reference_imps : path_kind -> identifier -> constr * int list
 
-val global : Environ.env -> identifier -> constr
+val construct_reference : Environ.env -> path_kind -> identifier -> constr
 
 val is_global : identifier -> bool