From 0447754621933102b7ec52e2b2c6c0320f911bba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 22 Sep 2017 18:33:46 +0200
Subject: Cannot unify message: improve preventing repeating twice the same
 message.

Call to nf_betaiota was done on one side of the comparison preventing
the same message to be repeated twice but not on the other side.
---
 vernac/himsg.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 12b68fe38..6d75b8ddd 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -300,6 +300,8 @@ let explain_unification_error env sigma p1 p2 = function
      | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
         (* Error speaks from itself *) []
      | ConversionFailed (env,t1,t2) ->
+        let t1 = Reductionops.nf_betaiota sigma t1 in
+        let t2 = Reductionops.nf_betaiota sigma t2 in
         if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
         let env = make_all_name_different env sigma in
         let t1 = Evarutil.nf_evar sigma t1 in
-- 
cgit v1.2.3