diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-14 01:14:27 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-14 01:59:25 +0100 |
commit | 7f9223bf9939a626b0813ecc6c34b4ef19b123f0 (patch) | |
tree | 2a699f00ea98b91f518597b3dc05c83c79e98670 /checker/cic.mli | |
parent | 8ea2a8307a8d96f8275ebbd9bd4cbd1f6b0a00c6 (diff) |
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.
Diffstat (limited to 'checker/cic.mli')
-rw-r--r-- | checker/cic.mli | 12 |
1 files changed, 12 insertions, 0 deletions
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 = { |