From f37ce408e943b29ab41c979a7f95ee824813397b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 9 Dec 2014 14:51:24 +0100
Subject: Added a CannotSolveConstraint unification error and made experiments
 in reporting the chain of causes when unification fails.

---
 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 9b5b79284b..21604a8fc2 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -22,6 +22,7 @@ type unification_error =
   | MetaOccurInBody of existential_key
   | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
+  | CannotSolveConstraint of Evd.evar_constraint * unification_error
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-- 
cgit v1.2.3