diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index d75af7654..881d3ca79 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -165,7 +165,10 @@ type action (** Engagements *) -type engagement = ImpredicativeSet +type set_predicativity = ImpredicativeSet | PredicativeSet +type type_hierarchy = TypeInType | StratifiedType + +type engagement = set_predicativity * type_hierarchy (** {6 Representation of constants (Definition/Axiom) } *) @@ -407,7 +410,7 @@ type compiled_library = { comp_name : compilation_unit_name; comp_mod : module_body; comp_deps : library_deps; - comp_enga : engagement option; + comp_enga : engagement; comp_natsymbs : nativecode_symb_array } |