From d87f8d10d089c3a33ddb36a71ab6fc082d0d1140 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2020 09:00:49 +0200
Subject: Fix GeoCoq slowdown.

There is no point in normalizing the goal in the legacy refiner because the
function is actually insensitive to evars.
---
 proofs/refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ad84afd47e..29a47c5acd 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -37,7 +37,7 @@ let refiner ~check =
       CProfile.profile2 refiner_key (refiner ~check)
   else refiner ~check
 
-let refiner ~check c = Proofview.V82.tactic (refiner ~check c)
+let refiner ~check c = Proofview.V82.tactic ~nf_evars:false (refiner ~check c)
 
 (*********************)
 (*   Tacticals       *)
-- 
cgit v1.2.3