From 1e67a490cd5ebbf5669e4cbf34a2a3066c0b5fc1 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 18 Jun 2012 14:52:27 +0000
Subject: Proof using: nested sections bugfix

It used to be the case that the list of declared section variables
for a constant was taken into account only when discharging the first
enclosing sections, but not any outer section. Example of the bug:

Section A. Variable x : bool.
Section B. Variable y : nat.
Lemma foo : True. Proof using x y. Admitted.
End B. End A.
Check foo. (* nat -> True instead of bool -> nat -> True *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15445 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cooking.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1a405e98ba..e79bc90bbc 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -136,6 +136,10 @@ let cook_constant env r =
     (fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps)
     cb.const_body
   in
+  let const_hyps =
+    Sign.fold_named_context (fun (h,_,_) hyps ->
+      List.filter (fun (id,_,_) -> id <> h) hyps)
+      hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | NonPolymorphicType t ->
 	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
@@ -146,4 +150,4 @@ let cook_constant env r =
 	let j = make_judge (constr_of_def body) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
-  (body, typ, cb.const_constraints)
+  (body, typ, cb.const_constraints, const_hyps)
-- 
cgit v1.2.3