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.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'kernel/cooking.mli') diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 5f31ff8ce..66927becc 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -22,7 +22,8 @@ type recipe = { d_modlist : work_list } val cook_constant : - env -> recipe -> constant_def * constant_type * constraints + env -> recipe -> + constant_def * constant_type * constraints * Sign.section_context (** {6 Utility functions used in module [Discharge]. } *) -- cgit v1.2.3