coq/bootstrap, branch master The formal proof system Cleaning of the new implementation of the tactic monad. 2014-08-04T13:56:38+00:00 Arnaud Spiwack 2014-08-04T13:44:19+00:00 94a759be56074ac66c5c96b0cc7722b395c4cf40 * Add comments in the code (mostly imported from Monad.v) * Inline duplicated module * Clean up some artifacts due to the extracted code. * [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally) * Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code). * Remove Monad.v 
* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v
Using the generic timeout function in the boostrapped file. 2014-07-15T13:46:48+00:00 Pierre-Marie Pédrot 2014-07-15T13:46:48+00:00 ec94edf830ff9676c43c86f0eb9038c4bd205f62 






Adding a [map] primitive to the tactic monad. Hopefully this should be
2014-04-20T19:11:17+00:00

Pierre-Marie Pédrot

2014-04-18T11:05:31+00:00

0f3f29792b8165b7eb89c049c76d065942739674

slightly more efficient in general.





slightly more efficient in general.







Transfering the initial goals from the proofview to the proof object.
2014-04-07T10:08:15+00:00

Pierre-Marie Pédrot

2014-04-07T10:08:15+00:00

61ee00dc214599ab6b17fac0586c746563eb565d

They were just passed along in the tactics.





They were just passed along in the tactics.







Adding an [modify] function to the tactic monad. It allows to modify
2014-04-06T16:11:27+00:00

Pierre-Marie Pédrot

2014-04-06T15:46:26+00:00

286984487d515cdb9f2e02834d23c65449760ba2

the current state without having to use both get, bind and set.





the current state without having to use both get, bind and set.







Fixing backtrace reporting.
2014-02-02T17:00:16+00:00

Pierre-Marie Pédrot

2014-02-02T16:59:39+00:00

2800a82dec607120fd2a378f7ac3bf4d6e8df18c












Fixing backtrace handling here and there.
2014-01-30T15:02:33+00:00

Pierre-Marie Pédrot

2014-01-30T14:30:01+00:00

1059ecce2a2662e4d8f335bd4db743df70b100b1












Cleanup of comments in bootstrap/Monads.v
2013-11-02T15:41:37+00:00

aspiwack

2013-11-02T15:41:37+00:00

7a7c00fdc81b450a5b2cb91b64bb2602d24212c1

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17031 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17031 85f007b7-540e-0410-9357-904b9bb8a0f7







Adds a tactic give_up.
2013-11-02T15:40:19+00:00

aspiwack

2013-11-02T15:40:19+00:00

fb1c2f25fb0ca5f422c69e14b6b434ad1d8f01a9

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





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







Adds a shelve tactic.
2013-11-02T15:39:54+00:00

aspiwack

2013-11-02T15:39:54+00:00

c9504af26647ab745dc22811a2db8058e0b66632

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





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