From 7f9223bf9939a626b0813ecc6c34b4ef19b123f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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.
---
 checker/cic.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'checker/cic.mli')

diff --git a/checker/cic.mli b/checker/cic.mli
index 4a0e706aa..95dd18f5f 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -170,6 +170,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet
 
 type engagement = set_predicativity
 
+(** {6 Conversion oracle} *)
+
+type level = Expand | Level of int | Opaque
+
+type oracle = {
+  var_opacity : level Id.Map.t;
+  cst_opacity : level Cmap.t;
+  var_trstate : Id.Pred.t;
+  cst_trstate : Cpred.t;
+}
+
 (** {6 Representation of constants (Definition/Axiom) } *)
 
 
@@ -219,6 +230,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 : oracle; (** Unfolding strategies for conversion *)
 }
 
 type constant_body = {
-- 
cgit v1.2.3