diff options
| author | Pierre-Marie Pédrot | 2019-03-18 10:31:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-18 10:31:24 +0100 |
| commit | 68dd7ff4aa71ac35a5023a2f3d471af08c0d276e (patch) | |
| tree | 6f97b7f26d6676d6c1db8b71a62eb88a9ca1bdaa | |
| parent | 0fc0b5f74a402c1393b485543eca6fbd63bafc61 (diff) | |
| parent | 05843c92e0fe96f09c7c4cb3d55376b99e6ea16b (diff) | |
Merge PR #9794: Use local universe names when printing universe inconsistency
Reviewed-by: ppedrot
| -rw-r--r-- | vernac/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 047bdd2b61..1c58abc2fd 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -308,7 +308,7 @@ let explain_unification_error env sigma p1 p2 = function | UnifUnivInconsistency p -> if !Constrextern.print_universes then [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p] + Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] else [str "universe inconsistency"] | CannotSolveConstraint ((pb,env,t,u),e) -> |