diff options
| author | Maxime Dénès | 2016-10-25 08:39:53 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-25 08:39:53 +0200 |
| commit | b00f7cdd1905e7d7c1f0241284f0808f8e1d2c45 (patch) | |
| tree | 24994922773f96baa2e644bbcc25ab01f686d41a /toplevel | |
| parent | b63a5cfa919fc0ebe664bbfb3add0fce387b1491 (diff) | |
| parent | 52a37da6b9e5d4e2024e31710df4e39cbd372865 (diff) | |
Merge remote-tracking branch 'github/pr/333' into v8.5
Was PR#233: Fix a bug in error printing of unif constraints
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 ae6c86c8cc..fe9b6d4e19 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 |