From 59263ca55924e2f43097ae2296f541b153981bf8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Dec 1999 09:23:34 +0000
Subject: correction bug construct_reference

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@219 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declare.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 5508432679..c756d6169f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -10,6 +10,8 @@ open Sign
 open Constant
 open Inductive
 open Reduction
+open Type_errors
+open Typeops
 open Libobject
 open Lib
 open Impargs
@@ -233,8 +235,10 @@ 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
   try
-    let (oper,_) = construct_operator env sp id in
-    let hyps = Global.var_context () in
+    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))
   with Not_found -> 
-- 
cgit v1.2.3