592eb02bb2
This PR makes the universe level pretty printer instantiate level metavariables when `pp.instantiateMVars` is true. Previously level metavariables were not instantiated. The PR adjusts the tracing in the LevelDefEq module to create the trace message using the original MetavarContext. It also adds `Meta.isLevelDefEq.step` traces for when level metavariables are assigned.
12 lines
199 B
Text
12 lines
199 B
Text
set_option pp.mvars false
|
|
|
|
/--
|
|
error: failed to solve universe constraint
|
|
u =?= 1
|
|
while trying to unify
|
|
Sort u : Type u
|
|
with
|
|
Type : Type 1
|
|
-/
|
|
#guard_msgs in
|
|
def A : Sort u := { s : Prop // _ }
|