From edcbdc62851c4ebef50ac8b2f67869f557e80242 Mon Sep 17 00:00:00 2001 From: gareuselesinge Date: Fri, 30 Aug 2013 12:20:12 +0000 Subject: 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 --- kernel/safe_typing.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/safe_typing.mli') 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 -- cgit v1.2.3