diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-10 18:05:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
| commit | b8a7222e670f69e024d50394afd88204e15d1b29 (patch) | |
| tree | 90c3c75ca9c2647ad41c6a30954cdf8ce3f6b5d8 /kernel/univ.mli | |
| parent | 1309723672def9bf322a23e9c789e4a8bc2a4ac3 (diff) | |
Less footguns in universe handling: remove subst_instance_context.
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index dc6fb85a0..3d0d2234d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -329,6 +329,9 @@ sig (** Keeps the order of the instances *) val union : t -> t -> t + val instantiate : Instance.t -> t -> Constraint.t + (** Generate the set of instantiated constraints **) + end type abstract_universe_context = AUContext.t @@ -443,7 +446,6 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context val make_instance_subst : universe_instance -> universe_level_subst val make_inverse_instance_subst : universe_instance -> universe_level_subst |