From 1f772656fa4bb6899ffea84ad5483e9690bbdc08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Jun 2016 16:00:23 +0200
Subject: Reserve exception "ConversionFailed" in unification for failure of
 conversion on closed terms.

This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
---
 pretyping/pretype_errors.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cf5b08c58f..b0715af734 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,15 +14,16 @@ open Type_errors
 
 type unification_error =
   | OccurCheck of existential_key * constr
-  | NotClean of existential * env * constr
+  | NotClean of existential * env * constr (* Constr is a variable not in scope *)
   | NotSameArgSize
   | NotSameHead
   | NoCanonicalStructure
-  | ConversionFailed of env * constr * constr
+  | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
   | MetaOccurInBody of existential_key
   | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency of Univ.univ_inconsistency
   | CannotSolveConstraint of Evd.evar_constraint * unification_error
+  | ProblemBeyondCapabilities
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-- 
cgit v1.2.3