diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-19 15:23:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-22 11:16:56 +0200 |
| commit | 52a37da6b9e5d4e2024e31710df4e39cbd372865 (patch) | |
| tree | 2ff3622497e3929fa39735f113dc2884114e4c16 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ae6c86c8c..fe9b6d4e1 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -741,7 +741,7 @@ let pr_constraints printenv env sigma evars cstrs = let evs = prlist (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr_env env' sigma evi.evar_concl) l + str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l in h 0 (pe ++ evs ++ pr_evar_constraints cstrs) else |