aboutsummaryrefslogtreecommitdiff
path: root/stm
AgeCommit message (Expand)Author
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-06-24Add corresponding field in `VernacInductive`.Arnaud Spiwack
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-06-09STM: states coming from workers have no proof terminators (Close #4246)Enrico Tassi
2015-06-09STM: silly mistake in jumping back to an old state (Close #4249)Enrico Tassi
2015-06-03Admitted does not drop poly-univ constraints (Fix #4244)Enrico Tassi
2015-05-28STM: preserve branch name on edit (Close: #4245, #4246)Enrico Tassi
2015-05-27Fix bug #4159Matthieu Sozeau
2015-05-12nice error for Restart outside a proof (Close: #4235)Enrico Tassi
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-04-21STM: print trace on "anomaly, no safe id attached"Enrico Tassi
2015-04-02Fix some typos.Guillaume Melquiond
2015-04-02CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Enrico Tassi
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-27STM: refine the notion of "simply a tactic"Enrico Tassi
2015-03-26STM: change how proof mode switching commands are handled (decl_mode)Enrico Tassi
2015-03-25STM: avoid processing asynchronously empty proofs (Close: #4134)Enrico Tassi
2015-03-22STM: if Set Universe Polymorphism then synchronous (#4119)Enrico Tassi
2015-03-22STM: do not delegate proofs containing PrintEnrico Tassi
2015-03-22STM: after every command restore the expected proof modeEnrico Tassi
2015-03-20Fixed #4138. In emacs mode Set/Unset does not print the goal anymore.Pierre Courtieu
2015-03-15STM: -debug: better explanation of why not async (#4125)Enrico Tassi
2015-03-15STM: -quick: async no Proof using but no Section (#4124)Enrico Tassi
2015-03-12Fixing bug #4055.Pierre-Marie Pédrot
2015-03-11STM: ease re-editing of Admitted proofsEnrico Tassi
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-27STM: Considering Stack_overflow as a normal tactic error (Close #3576)Enrico Tassi
2015-02-25STM: proof state also includes meta countersEnrico Tassi
2015-02-21Future: human readable name for delegated (Close #4065)Enrico Tassi
2015-02-16STM: when async_proofs_full is set process only tasks in the perspectiveEnrico Tassi
2015-02-16*Queue: API to wake up all threadsEnrico Tassi
2015-02-15Undo: back to 8.4 semantics (Close #3514)Enrico Tassi
2015-02-15Reset "section name" works again (Close #3933)Enrico Tassi
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-11STM: is Flags.async_proofs_full then always delegateEnrico Tassi
2015-02-10Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq...Hugo Herbelin
2015-02-09Fix bug #4014.Pierre-Marie Pédrot
2015-02-07STM: tolerate simple side effects in async proofs (Close: 4006)Enrico Tassi
2015-02-05Fix automatic undo after nonsensical Qed in tty mode (Close: 3980)Enrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-09STM: fix handling of side effects in vio2voEnrico Tassi
2015-01-07Hook when state arrives on master.Enrico Tassi
2015-01-06rename: vi -> vioEnrico Tassi
2015-01-04STM: Make assert unneeded (Close 3898)Enrico Tassi
2014-12-27STM: check with the kernel proof terms on the worker tooEnrico Tassi
2014-12-27STM: fix processing of errorsEnrico Tassi
2014-12-27STM: module Pp is openEnrico Tassi
2014-12-26STM: do not call process_error twice (Close: 3880)Enrico Tassi
2014-12-26STM: remove dead codeEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 15:21:37 +0000