diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 17:33:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:23:04 +0100 |
| commit | bad3f3b784d3de8851615b8f4b7afba734232d8e (patch) | |
| tree | be6a12a50d3bf6b73ea7866334585f694370e630 /engine/universes.mli | |
| parent | 441bea723c511ed9e18ef005678bd01242b45c49 (diff) | |
Moving some universe substitution code out of the kernel.
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 1a98d969b..130dcf8bb 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -154,6 +154,11 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> module UF : Unionfind.PartitionSig with type elt = Level.t +val level_subst_of : universe_subst_fn -> universe_level_subst_fn +val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t + +val subst_univs_constr : universe_subst -> constr -> constr + type universe_opt_subst = Universe.t option universe_map val make_opt_subst : universe_opt_subst -> universe_subst_fn |