diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 629d83fb8..b68bbdf35 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -128,12 +128,6 @@ sig val map : (Level.t * int -> 'a) -> t -> 'a list - (** [compact u] remaps local variables in [u] such that their indices become - consecutive. It returns the new universe and the mapping. - Example: compact [(Var 0, i); (Prop, 0); (Var 2; j))] = - [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] - *) - val compact : t -> t * int list end type universe = Universe.t @@ -211,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function Constraint.t... *) type explanation = (constraint_type * Universe.t) list -type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option +type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency @@ -504,6 +498,13 @@ val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativit val make_abstract_instance : AUContext.t -> Instance.t +(** [compact_univ u] remaps local variables in [u] such that their indices become + consecutive. It returns the new universe and the mapping. + Example: compact_univ [(Var 0, i); (Prop, 0); (Var 2; j))] = + [(Var 0,i); (Prop, 0); (Var 1; j)], [0; 2] +*) +val compact_univ : Universe.t -> Universe.t * int list + (** {6 Pretty-printing of universes. } *) val pr_constraint_type : constraint_type -> Pp.t |