diff options
| author | Pierre-Marie Pédrot | 2018-09-11 11:00:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-21 13:09:21 +0200 |
| commit | 51dad02266f0bea735d496839c559b472bc4553e (patch) | |
| tree | a6a18abe9b8d1ee74c848f6dcd302c08adb89da6 /vernac | |
| parent | 4c28e0597067d81f5ee7e8b2b2e668f4d45e973f (diff) | |
Removing calls to AUContext.instance.
We simply declare the bound universes with their user-facing name in the
evarmap and call all printing functions on uninstantiated terms. We had to
tweak the universe name declaring function so that it would work properly
with bound universe variables and handle sections correctly.
This changes the output of polymorphic definitions with unnamed universe
variables. Now they are printed as Var(i) instead of the Module.n uid
that came from their absolute name.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a4650cfd92..1b6d12a976 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -896,7 +896,8 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in + let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in + (** FIXME: provide a proper naming for the bound variables *) quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = |