diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 10:25:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-20 17:45:22 +0200 |
| commit | 513e194656429b6a9142a3a34095cee2c6f8ee96 (patch) | |
| tree | a935129d675b538a12102e1cddac453a05f6b76e /toplevel | |
| parent | 283579ff70d324296e2b7ee2535b1187ca32e0cb (diff) | |
Fixing an anomaly in printing a unification error message.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 13a6489b9..ae6c86c8c 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -307,6 +307,7 @@ let rec explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in + let env = make_all_name_different env in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e |