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/declarations.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/declarations.ml') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7f4b85fd0..5b9e1a141 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -74,6 +74,7 @@ type typing_flags = { check_guarded : bool; (** If [false] then fixed points and co-fixed points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) + conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) } (* some contraints are in constant_constraints, some other may be in -- cgit v1.2.3