diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-22 18:33:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-22 18:41:48 +0200 |
| commit | 0447754621933102b7ec52e2b2c6c0320f911bba (patch) | |
| tree | 344a4f46b5ff1d2b6cb1c7b7913d306cd1401d80 /vernac/himsg.ml | |
| parent | 7e4535d62c4f8abc6537206e7abc34f1bb0be69d (diff) | |
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.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |