aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.mli')
-rw-r--r--kernel/safe_typing.mli3
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