diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /engine/universes.mli | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index c600f4af6..5ce5e4a42 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -101,10 +101,10 @@ val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrai (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -val fresh_instance_from_context : universe_context -> +val fresh_instance_from_context : abstract_universe_context -> universe_instance constrained -val fresh_instance_from : universe_context -> universe_instance option -> +val fresh_instance_from : abstract_universe_context -> universe_instance option -> universe_instance in_universe_context_set val fresh_sort_in_family : env -> sorts_family -> @@ -228,4 +228,4 @@ val solve_constraints_system : universe option array -> universe array -> univer (** Given a universe context representing constraints of an inductive this function produces a UInfoInd.t that with the trivial subtyping relation. *) -val univ_inf_ind_from_universe_context : universe_context -> universe_info_ind +val univ_inf_ind_from_universe_context : universe_context -> cumulativity_info |