diff options
| author | Pierre-Marie Pédrot | 2018-09-27 14:23:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-09 14:10:27 +0100 |
| commit | 601ce3738253e4bb197900ee6dad271c4e3666d6 (patch) | |
| tree | c4164f53de30589a26a147f548b8693875971027 /kernel/univ.mli | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
Adding universe names to polymorphic entry instances.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 7ac8247ca4..bc902d8f4b 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -347,6 +347,9 @@ sig val instantiate : Instance.t -> t -> Constraint.t (** Generate the set of instantiated Constraint.t **) + val names : t -> Names.Name.t list + (** Return the names of the bound universe variables *) + end (** Universe info for cumulative inductive types: A context of |