From cb635eab423cde23757725593ffdfb98f4016881 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 7 Mar 2017 18:13:07 +0100
Subject: Fix an optimization failure in tclPROGRESS.

Due to code reworking, a fastpath got anihilated because the slow path
was computed altogether. We now only compute the slow check whenever the
quick one fails.
---
 engine/proofview.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index c01879765b..2e6266cf15 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -828,14 +828,12 @@ let tclPROGRESS t =
   let quick_test =
     initial.solution == final.solution && initial.comb == final.comb
   in
-  let exhaustive_test =
+  let test =
+    quick_test ||
     Util.List.for_all2eq begin fun i f ->
       Progress.goal_equal initial.solution i final.solution f
     end initial.comb final.comb
   in
-  let test =
-    quick_test || exhaustive_test
-  in
   if not test then
     tclUNIT res
   else
-- 
cgit v1.2.3