diff options
| author | Enrico Tassi | 2014-12-28 14:02:38 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-28 14:02:38 +0100 |
| commit | 8405bdf08e04792a290d1517591ab3fc2945deb7 (patch) | |
| tree | 7d66eeab16acdf3902f029b8a4e4d5a27746335c | |
| parent | 5196c281298a3168b84f1df26b71f07c873f4b5d (diff) | |
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.
| -rw-r--r-- | proofs/proof_global.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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... *) |