diff options
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 |