aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
Commit message (Expand)AuthorAge
* Add corresponding field in `VernacInductive`.Gravatar Arnaud Spiwack2015-06-24
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* STM: states coming from workers have no proof terminators (Close #4246)Gravatar Enrico Tassi2015-06-09
* STM: silly mistake in jumping back to an old state (Close #4249)Gravatar Enrico Tassi2015-06-09
* Admitted does not drop poly-univ constraints (Fix #4244)Gravatar Enrico Tassi2015-06-03
* STM: preserve branch name on edit (Close: #4245, #4246)Gravatar Enrico Tassi2015-05-28
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* nice error for Restart outside a proof (Close: #4235)Gravatar Enrico Tassi2015-05-12
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* STM: print trace on "anomaly, no safe id attached"Gravatar Enrico Tassi2015-04-21
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* STM: refine the notion of "simply a tactic"Gravatar Enrico Tassi2015-03-27
* STM: change how proof mode switching commands are handled (decl_mode)Gravatar Enrico Tassi2015-03-26
* STM: avoid processing asynchronously empty proofs (Close: #4134)Gravatar Enrico Tassi2015-03-25
* STM: if Set Universe Polymorphism then synchronous (#4119)Gravatar Enrico Tassi2015-03-22
* STM: do not delegate proofs containing PrintGravatar Enrico Tassi2015-03-22
* STM: after every command restore the expected proof modeGravatar Enrico Tassi2015-03-22
* Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.Gravatar Pierre Courtieu2015-03-20
* STM: -debug: better explanation of why not async (#4125)Gravatar Enrico Tassi2015-03-15
* STM: -quick: async no Proof using but no Section (#4124)Gravatar Enrico Tassi2015-03-15
* Fixing bug #4055.Gravatar Pierre-Marie Pédrot2015-03-12
* STM: ease re-editing of Admitted proofsGravatar Enrico Tassi2015-03-11
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* STM: Considering Stack_overflow as a normal tactic error (Close #3576)Gravatar Enrico Tassi2015-02-27
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Future: human readable name for delegated (Close #4065)Gravatar Enrico Tassi2015-02-21
* STM: when async_proofs_full is set process only tasks in the perspectiveGravatar Enrico Tassi2015-02-16
* *Queue: API to wake up all threadsGravatar Enrico Tassi2015-02-16
* Undo: back to 8.4 semantics (Close #3514)Gravatar Enrico Tassi2015-02-15
* Reset "section name" works again (Close #3933)Gravatar Enrico Tassi2015-02-15
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* STM: is Flags.async_proofs_full then always delegateGravatar Enrico Tassi2015-02-11
* Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...Gravatar Hugo Herbelin2015-02-10
* Fix bug #4014.Gravatar Pierre-Marie Pédrot2015-02-09
* STM: tolerate simple side effects in async proofs (Close: 4006)Gravatar Enrico Tassi2015-02-07
* Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)Gravatar Enrico Tassi2015-02-05
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* STM: fix handling of side effects in vio2voGravatar Enrico Tassi2015-01-09
* Hook when state arrives on master.Gravatar Enrico Tassi2015-01-07
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* STM: Make assert unneeded (Close 3898)Gravatar Enrico Tassi2015-01-04
* STM: check with the kernel proof terms on the worker tooGravatar Enrico Tassi2014-12-27
* STM: fix processing of errorsGravatar Enrico Tassi2014-12-27
* STM: module Pp is openGravatar Enrico Tassi2014-12-27
* STM: do not call process_error twice (Close: 3880)Gravatar Enrico Tassi2014-12-26
* STM: remove dead codeGravatar Enrico Tassi2014-12-26
* Inlining Spawn.kill_if in the one place were it was actually used, thusGravatar Pierre-Marie Pédrot2014-12-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 08:05:37 +0000