diff options
| author | Pierre-Marie Pédrot | 2018-11-19 13:51:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-19 13:51:59 +0100 |
| commit | f9a890aa9ff9d199bd6c98ee33274894fd5d8972 (patch) | |
| tree | cabbb7c9767a7c6b12862fbf36a54c3cc6077f47 /engine | |
| parent | 1ca5089ebc8250073575ba0b63242a36e66a803e (diff) | |
| parent | 3d49ce63bd1aa35ef2e8abc9cc359ad6031c21bb (diff) | |
Merge PR #8894: Print full binders in subtyping incompatible polymorphism error.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univNames.ml | 8 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
2 files changed, 3 insertions, 7 deletions
diff --git a/engine/univNames.ml b/engine/univNames.ml index ad91d31f87..1019f8f0c2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -36,10 +36,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_of_global ref : Name.t array = - try AUContext.names (Environ.universes_of_global (Global.env ()) ref) - with Not_found -> [||] - let name_universe lvl = (** Best-effort naming from the string representation of the level. This is completely hackish and should be solved in upper layers instead. *) @@ -55,8 +51,8 @@ let compute_instance_binders inst ubinders = type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref names = - let orig = universe_binders_of_global ref in +let universe_binders_with_opt_names orig names = + let orig = AUContext.names orig in let orig = Array.to_list orig in let udecl = match names with | None -> orig 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 |