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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index f617df9ee7..880f48e5f9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,6 +24,7 @@ type unification_error =
   | 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