Fixing an anomaly in printing a unification error message.

2 files changed, 9 insertions, 0 deletions

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