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/evarsolve.ml       | 10 +++++++---
 pretyping/pretype_errors.ml  |  1 +
 pretyping/pretype_errors.mli |  1 +
 3 files changed, 9 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 0e1ecda5cf..c62d567904 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1497,10 +1497,14 @@ let status_changed lev (pbty,_,t1,t2) =
 let reconsider_conv_pbs conv_algo evd =
   let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
   List.fold_left
-    (fun p (pbty,env,t1,t2) ->
+    (fun p (pbty,env,t1,t2 as x) ->
        match p with
-       | Success evd -> conv_algo env evd pbty t1 t2
-       | UnifFailure _ as x -> x) (Success evd)
+       | Success evd ->
+           (match conv_algo env evd pbty t1 t2 with
+           | Success _ as x -> x
+           | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
+       | UnifFailure _ as x -> x)
+    (Success evd)
     pbs
 
 (* Tries to solve problem t1 = t2.
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
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 1222406217..741279a512 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -23,6 +23,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