From adc2035410a339cfa88dae527b631f5131adaa54 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/proofview.ml')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index f054038e9c..99bd4bc4ff 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -858,14 +858,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