From 8405bdf08e04792a290d1517591ab3fc2945deb7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 28 Dec 2014 14:02:38 +0100
Subject: Call nf_constraints also when compiling directly to vo

After commit b46944e the system got way slower, hence the optimization
is relevant also for non polymorphic constants.  Putting it back now,
but we shall find something in between: an optimization that does
not clash with async proofs but that gives some performance improvement
over no optimization at all.
---
 proofs/proof_global.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 07ff6e41ad..f81abe5ed2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -354,7 +354,10 @@ let return_proof () =
         error(str"Attempt to save a proof with existential " ++
               str"variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
-  let evd = if poly then Evd.nf_constraints evd else evd in
+  let evd =
+    if poly || !Flags.compilation_mode = Flags.BuildVo
+    then Evd.nf_constraints evd
+    else evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
       side-effects... This may explain why one need to uniquize side-effects
       thereafter... *)
-- 
cgit v1.2.3