From 60ec0e0a67e60c52af7e7ef34a2826ef7fb61a26 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 26 Feb 2020 14:20:24 +0100
Subject: Remove spurious anomalies in kernel reduction

---
 kernel/reduction.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5fbe501169..66c4067506 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -354,7 +354,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         (match kind a1, kind a2 with
            | (Sort s1, Sort s2) ->
                if not (is_empty_stack v1 && is_empty_stack v2) then
-                 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
+                 (* May happen because we convert application right to left *)
+                 raise NotConvertible;
               sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
            | (Meta n, Meta m) ->
                if Int.equal n m
@@ -471,7 +472,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
-          anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
+          (* May happen because we convert application right to left *)
+          raise NotConvertible;
         (* Luo's system *)
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
-- 
cgit v1.2.3