construct_reference prend en compte aussi les variables du context

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

1 files changed, 10 insertions, 10 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 2ccd77cf0..f186aa18c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -239,20 +239,20 @@ let construct_operator env sp id =
 let global_operator sp id = construct_operator (Global.env()) sp id
 
 let construct_sp_reference env sp id =
+  let (oper,hyps) = construct_operator env sp id in
+  let hyps' = Global.var_context () in
+  if not (hyps_inclusion env Evd.empty hyps hyps') then
+    error_reference_variables CCI env id;
+  let ids = ids_of_sign hyps in
+  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+
+let construct_reference env kind id =
   try
-    let (oper,hyps) = construct_operator env sp id in
-    let hyps' = Global.var_context () in
-    if not (hyps_inclusion env Evd.empty hyps hyps') then
-      error_reference_variables CCI env id;
-    let ids = ids_of_sign hyps in
-    DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+    let sp = Nametab.sp_of_id kind id in
+    construct_sp_reference env sp id
   with Not_found -> 
     VAR (let _ = Environ.lookup_var id env in id)
 
-let construct_reference env kind id =
-  let sp = Nametab.sp_of_id kind id in
-  construct_sp_reference env sp id
-
 let global_sp_reference sp id = 
   construct_sp_reference (Global.env()) sp id