From e6404437c1f6ae451f4253cd3450f75513b395c3 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:35:34 +0000 Subject: Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by extraction. The goal was to use Coq's partial evaluation capabilities to do manually some inlining that Ocaml couldn't do. It may be critical as we are defining higher order combinators in term of others and no inlining means a lot of unnecessary, short-lived closures built. With this modification we get back some (but not all) of the loss of performance introduced by threading the monadic type all over the place. I still have an estimated 15% longer compilation time for Coq. Makes use of Set Extraction Conservative Types and Set Extraction File Comment to maintain the relationship between the functions and their types. Uses an intermediate layer Proofview_monad between Proofview_gen and Proofview in order to use a hand-written mli to catch potential errors in the generated file (it uses Extract Constant a lot). A bug in the extraction of signatures forces to remove the generated proofview_gen.mli which does not have the correct types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16981 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/proofs.mllib | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'proofs/proofs.mllib') diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 19f289316..4a7efb029 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,7 +1,9 @@ Goal Evar_refiner -Monads Proof_type +Proof_errors +Proofview_gen +Proofview_monad Proofview Proof Proof_global -- cgit v1.2.3