From 52a37da6b9e5d4e2024e31710df4e39cbd372865 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 19 Oct 2016 15:23:40 +0200 Subject: 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. --- toplevel/himsg.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') 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 -- cgit v1.2.3