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 /engine/univNames.mli | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
Adding universe names to polymorphic entry instances.
Diffstat (limited to 'engine/univNames.mli')
| -rw-r--r-- | engine/univNames.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli index bd4062ade4..634db9581c 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,6 +19,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders +val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list + val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit type univ_name_list = Names.lname list |