From 456919dd31f2f4bda15c6b37e4f1217bc085fc41 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Oct 2018 16:13:31 +0200
Subject: Switch order eqappr/check relevance in conversion.

This takes advantage of the mutability of the fconstr relevance mark.
---
 kernel/reduction.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f32531721c..8c364602e9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -329,9 +329,8 @@ let is_irrelevant infos lft c =
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
-  if is_irrelevant infos lft1 term1 && is_irrelevant infos lft2 term2
-  then cuniv
-  else eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+  try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+  with NotConvertible when is_irrelevant infos lft1 term1 && is_irrelevant infos lft2 term2 -> cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
 and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
-- 
cgit v1.2.3