From ea8185d872f242f8ebf4274ebe550ed81107150a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 12 Mar 2017 19:57:48 +0100 Subject: Making the side_effects type opaque. We move it from Entries to Term_typing and export the few functions needed to manipulate it in this module. --- kernel/safe_typing.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/safe_typing.mli') diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 15ebc7d88..8bc47d6ce 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -47,7 +47,7 @@ type private_constant_role = | Schema of inductive * string val side_effects_of_private_constants : - private_constants -> Entries.side_effects + private_constants -> Entries.side_effect list val empty_private_constants : private_constants val add_private : private_constant -> private_constants -> private_constants -- cgit v1.2.3