diff options
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 7651e34b12..7286fc84cb 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -353,6 +353,10 @@ module AUContext : sig type t + val make : Names.Name.t array -> Constraint.t -> t + (** Build an abstract context. Constraints may be between universe + variables. *) + val repr : t -> UContext.t (** [repr ctx] is [(Var(0), ... Var(n-1) |= cstr] where [n] is the length of the context and [cstr] the abstracted Constraint.t. *) |