diff options
| author | Matthieu Sozeau | 2016-10-19 15:23:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-22 11:16:56 +0200 |
| commit | 52a37da6b9e5d4e2024e31710df4e39cbd372865 (patch) | |
| tree | 2ff3622497e3929fa39735f113dc2884114e4c16 /kernel/cemitcodes.ml | |
| parent | 5609da1e08f950fab85b87b257ed343b491f1ef5 (diff) | |
Fix a bug in error printing of unif constraints
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions