diff options
| author |  gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:12 +0000 |
|---|---|---|
| committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-30 12:20:12 +0000 |
| commit | edcbdc62851c4ebef50ac8b2f67869f557e80242 (patch) | |
| tree | 47038bc43d6f385ea5fe8d16ef690fbe3b4255ee /kernel/safe_typing.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/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5d1c98de5..a56bb8578 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -34,6 +34,9 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) val sideff_of_con : safe_environment -> constant -> Declarations.side_effect +val sideff_of_scheme : + string -> safe_environment -> (inductive * constant) list -> + Declarations.side_effect val is_curmod_library : safe_environment -> bool |