From 7f9223bf9939a626b0813ecc6c34b4ef19b123f0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 14 Jan 2018 01:14:27 +0100 Subject: Store the conversion oracle in constant and inductive definitions. We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet. --- kernel/declareops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/declareops.mli') diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 198831848..0eed11f49 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -67,7 +67,7 @@ val inductive_is_cumulative : mutual_inductive_body -> bool (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) -val safe_flags : typing_flags +val safe_flags : Conv_oracle.oracle -> typing_flags (** {6 Hash-consing} *) -- cgit v1.2.3