diff options
| author | gareuselesinge | 2011-12-12 14:00:45 +0000 |
|---|---|---|
| committer | gareuselesinge | 2011-12-12 14:00:45 +0000 |
| commit | 7e1fefc0a095f7bb7f720218f9d472d4b0d6507d (patch) | |
| tree | a853d983f64e85d752d771df1e8f2044879a6ca2 /kernel/entries.ml | |
| parent | dc8f9bb9033702dc7552450c5a3891fd060ee001 (diff) | |
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
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 28f11c9af4..a4485fac7f 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -56,12 +56,13 @@ type mutual_inductive_entry = { type definition_entry = { const_entry_body : constr; + const_entry_secctx : section_context option; const_entry_type : types option; const_entry_opaque : bool } type inline = int option (* inlining level, None for no inlining *) -type parameter_entry = types * inline +type parameter_entry = section_context option * types * inline type constant_entry = | DefinitionEntry of definition_entry |