From cade097ff6e5670b5f4c3ea832b593cf88251fbd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Dec 2020 18:21:49 +0100
Subject: Fast path in tclPROGRESS.

We first check that the list of goals have the same length before trying to
engage into potentially costly equality checks.
---
 engine/proofview.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 22863f451d..b3061eaa81 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -909,10 +909,11 @@ let tclPROGRESS t =
   in
   let test =
     quick_test ||
+    (CList.same_length initial.comb final.comb &&
     Util.List.for_all2eq begin fun i f ->
       Progress.goal_equal ~evd:initial.solution
         ~extended_evd:final.solution (drop_state i) (drop_state f)
-    end initial.comb final.comb
+    end initial.comb final.comb)
   in
   if not test then
     tclUNIT res
-- 
cgit v1.2.3