diff options
| author | gareuselesinge | 2013-08-30 12:20:12 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-30 12:20:12 +0000 |
| commit | edcbdc62851c4ebef50ac8b2f67869f557e80242 (patch) | |
| tree | 47038bc43d6f385ea5fe8d16ef690fbe3b4255ee /kernel/declarations.mli | |
| parent | 6a5b186d2b53cf2c3e3a7ed5c238d26367a9df96 (diff) | |
ind_tables: properly handling side effects
If a constant is defined as transparent, not only its side effects
(opaque sub proofs as in abstract, and transparent ind schemes)
are declared globally, but the ones that are schemes are also declared
as such.
The only sub optimal thing is that the code handling in a special
way the side effects of transparent constants is in declare.ml that
does not see ind_tables.ml, hence a forward ref to a function is used.
IMO, ind_tables has no reason to stay in toplevel/.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 6a5b0dbb20..d74c9a0d5e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -59,7 +59,9 @@ type constant_body = { const_native_name : native_name ref; const_inline_code : bool } -type side_effect = NewConstant of constant * constant_body +type side_effect = + | SEsubproof of constant * constant_body + | SEscheme of (inductive * constant * constant_body) list * string (** {6 Representation of mutual inductive types in the kernel } *) |