From 23cd71a9d75e8307b0d85e9e287706cbc7b96ae9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 6 May 2019 00:35:56 +0200
Subject: Coqchk: encapsulating an anomaly NotConvertible into a proper typing
 error.

Detected incidentally in "validate" check for #8893.
---
 checker/mod_checking.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b86d491d72..1dd16f1630 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -33,7 +33,8 @@ let check_constant_declaration env kn cb =
     match Environ.body_of_constant_body env cb with
     | Some bd ->
       let j = infer env' (fst bd) in
-      conv_leq env' j.uj_type ty
+      (try conv_leq env' j.uj_type ty
+       with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()
   in
   let env =
-- 
cgit v1.2.3