diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 90a0e9fe..bd75111a 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -102,7 +102,7 @@ type constr = | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint - | Proj of constant * constr + | Proj of projection * constr type existential = constr pexistential type rec_declaration = constr prec_declaration @@ -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) } *) @@ -377,7 +380,7 @@ and module_body = (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; mod_retroknowledge : action list } @@ -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 } @@ -417,12 +420,16 @@ type compiled_library = { type library_objects -type library_disk = { +type summary_disk = { md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : library_deps; +} + +type library_disk = { md_compiled : compiled_library; md_objects : library_objects; - md_deps : library_deps; - md_imports : compilation_unit_name array } +} type opaque_table = constr Future.computation array type univ_table = |