From 513e194656429b6a9142a3a34095cee2c6f8ee96 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 20 Aug 2016 10:25:37 +0200 Subject: Fixing an anomaly in printing a unification error message. --- test-suite/success/Case13.v | 8 ++++++++ toplevel/himsg.ml | 1 + 2 files changed, 9 insertions(+) diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8e..8f95484cf 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. 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 -- cgit v1.2.3