From f9e68540f9673e5165f9a22fc93d9f7ebf7f1519 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Thir=C3=A9?=
 <francois.thire@nomadic-labs.com>
Date: Thu, 16 Jun 2022 14:15:30 +0200
Subject: [PATCH] Kernel: Optimise conversion

---
 kernel/reduction.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3ad91de1..0b63c981 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -504,8 +504,12 @@ module Make (C : ConvChecker) (M : Matching.Matcher) : S = struct
   let rec are_convertible_lst sg : (term * term) list -> bool = function
     | [] -> true
     | (t1, t2) :: lst ->
+        (* Check physical equality first for optimisation. *)
         are_convertible_lst sg
-          (if term_eq t1 t2 then lst
+          (if t1 == t2 then lst
+           (* This test can be less expensive than computing the `whnf` if the
+              two terms are equal. *)
+          else if term_eq t1 t2 then lst
           else conversion_step sg (whnf sg t1, whnf sg t2) lst)
 
   (* Convertibility Test *)