| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Benefits: fewer pair constructed/destructed especially in split.
Potential costs: plus and zero now have closures with 11 arguments.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17012 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
style.
Benefits: the underlying monads are not referenced in the "current" primitive.
Potential costs: some extracted functions now have 9 arguments, Ocaml may not be good at handling these. The split primitive, which is called often, now builds one extra closure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
It doesn't seem to affect performances. But the generated code is slightly cleaner.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Exchanges a IO.bind for a Logic.bind. The latter is better inlined.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16995 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Instead of interleaving the reifications and reflection steps, split is defined as a series of reification followed by a series of reflection.
The immediate consequence is that split is hoisted out of the Logic interface, and defined in a single block at the end of the file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Reduces the size of split significantly. In particular it now uses only 2 matches instead of 4.
Patch by Pierre-Marie Pédrot and Pierre Letouzey.
Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16993 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
Explanations here: https://ocaml.janestreet.com/?q=node/30
Patch by Pierre-Marie Pédrot, with modifications from Arnaud Spiwack.
Signed-off-by: Arnaud Spiwack <arnaud@spiwack.net>
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16989 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
This is just a port of the existing design. Basing the tactics on an IO monad
may allow to simplify things a bit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
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
|
aspiwack