From 772aa6bd5659d466b92ea33c997012414b0f946c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 16 Sep 2020 15:05:12 +0200
Subject: More precise information when unification fails because of
 incompatible candidates.

We also show the incompatible contender.

Ideally, we should also remember the source of the other contender.
---
 pretyping/pretype_errors.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 207ffc7b86..1e8441dd8a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -20,6 +20,7 @@ type unification_error =
   | NotSameHead
   | NoCanonicalStructure
   | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
+  | IncompatibleInstances of env * existential * constr * constr
   | MetaOccurInBody of Evar.t
   | InstanceNotSameType of Evar.t * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
-- 
cgit v1.2.3