From 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 12 Dec 2011 14:00:45 +0000
Subject: Proof using ...

New vernacular "Proof using idlist" to declare the variables
to be discharged at the end of the current proof. The system
checks that the set of declared variables is a superset of
the set of actually used variables.

It can be combined in a single line with "Proof with":
Proof with .. using ..
Proof using .. with ..

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term_typing.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/term_typing.mli')

diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 158f2c7877..3bbf566774 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,11 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry ->
-  constant_def * constant_type * constraints
+  constant_def * constant_type * constraints * Sign.section_context option
 
 val build_constant_declaration : env -> 'a ->
-  constant_def * constant_type * constraints -> constant_body
+  constant_def * constant_type * constraints * Sign.section_context option -> 
+    constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body
 
-- 
cgit v1.2.3