diff options
| author | Gaëtan Gilbert | 2018-11-13 16:25:23 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 15:09:52 +0100 |
| commit | 3d49ce63bd1aa35ef2e8abc9cc359ad6031c21bb (patch) | |
| tree | c3750e4aae2d3c0b14879090e001b6cbc1b8c769 /engine/univNames.mli | |
| parent | 744a07e53fb99652b2b30520cfe3dfe701bbde18 (diff) | |
Print universe names in subtyping error instead of Var(x).
Diffstat (limited to 'engine/univNames.mli')
| -rw-r--r-- | engine/univNames.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/univNames.mli b/engine/univNames.mli index dc669f45d6..6e68153ac2 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -29,5 +29,5 @@ type univ_name_list = Names.lname list of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. Otherwise return the bound universe names registered for [ref]. *) -val universe_binders_with_opt_names : Names.GlobRef.t -> +val universe_binders_with_opt_names : AUContext.t -> univ_name_list option -> universe_binders |