| Age | Commit message (Expand) | Author |
|---|
| 2016-05-04 | Fix for #4603, part 3: definitions inside proofs not handled properly by coqc. | Maxime Dénès |
| 2016-04-15 | Build stm debugging messages lazily so that they are not silently | Hugo Herbelin |
| 2016-04-12 | Quick fix for #4603 (part 2): Anomaly: Universe undefined | Maxime Dénès |
| 2016-02-19 | STM: Print/Extraction have to be skipped if -quick | Enrico Tassi |
| 2016-02-19 | STM: classify some variants of Instance as regular `Fork nodes. | Enrico Tassi |
| 2016-02-10 | STM: always stock in vio files the first node (state) of a proof | Enrico Tassi |
| 2016-02-10 | STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530 | Enrico Tassi |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-15 | Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. | Maxime Dénès |
| 2016-01-04 | fixup d2b468a, evar normalization is needed | Enrico Tassi |
| 2016-01-04 | par: check if the goal is not ground and fail (fix #4465) | Enrico Tassi |
| 2015-11-02 | Follow-up fix on Enrico's 6e376c8097d75b6e, with Enrico. | Maxime Dénès |
| 2015-11-02 | STM: fix undo into a branch containing side effects | Enrico Tassi |
| 2015-11-02 | STM: never reopen a branch containing side effects | Enrico Tassi |
| 2015-10-30 | Add a way to get the right fix_exn in external vernacular commands | Matthieu Sozeau |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin |
| 2015-10-09 | STM: Work around an occasional crash in dot (debug output) | Alec Faithfull |
| 2015-10-09 | STM: Added functions for saving and restoring the internal state | Alec Faithfull |
| 2015-10-09 | STM: Pass exception information to unreachable_state_hook functions | Alec Faithfull |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-10-08 | STM: for PIDE based UIs, edit_at requires no Reach.known_state | Enrico Tassi |
| 2015-10-08 | STM: fix backtrace handling | Enrico Tassi |
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau |
| 2015-09-01 | STM: save a full state for queries. | Enrico Tassi |
| 2015-07-30 | STM: make multiple, admitted, nested proofs work (fix #4314) | Enrico Tassi |
| 2015-07-30 | STM: emit a warning when a QED/Admitted proof contains a nested lemma | Enrico Tassi |
| 2015-07-30 | STM: fix backtrack in presence of nested, immediate, proofs | Enrico Tassi |
| 2015-07-30 | STM: remove assertion not being true for nested, immediate, proofs (#4313) | Enrico Tassi |
| 2015-07-29 | Fixing what seems to be a typo. | Hugo Herbelin |
| 2015-07-28 | ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308) | Enrico Tassi |
| 2015-07-14 | STM: fix a "exn with no safe id attached" error on a failing query | Enrico Tassi |
| 2015-06-09 | STM: states coming from workers have no proof terminators (Close #4246) | Enrico Tassi |
| 2015-06-09 | STM: silly mistake in jumping back to an old state (Close #4249) | Enrico Tassi |
| 2015-05-28 | STM: preserve branch name on edit (Close: #4245, #4246) | Enrico Tassi |
| 2015-05-12 | nice error for Restart outside a proof (Close: #4235) | Enrico Tassi |
| 2015-05-04 | Add a [Redirect] vernacular command | Clément Pit--Claudel |
| 2015-04-21 | STM: print trace on "anomaly, no safe id attached" | Enrico Tassi |
| 2015-04-02 | CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168) | Enrico Tassi |
| 2015-03-27 | STM: refine the notion of "simply a tactic" | Enrico Tassi |
| 2015-03-26 | STM: change how proof mode switching commands are handled (decl_mode) | Enrico Tassi |
| 2015-03-25 | STM: avoid processing asynchronously empty proofs (Close: #4134) | Enrico Tassi |
| 2015-03-22 | STM: if Set Universe Polymorphism then synchronous (#4119) | Enrico Tassi |
| 2015-03-22 | STM: do not delegate proofs containing Print | Enrico Tassi |
| 2015-03-22 | STM: after every command restore the expected proof mode | Enrico Tassi |
| 2015-03-20 | Fixed #4138. In emacs mode Set/Unset does not print the goal anymore. | Pierre Courtieu |
| 2015-03-15 | STM: -debug: better explanation of why not async (#4125) | Enrico Tassi |
| 2015-03-15 | STM: -quick: async no Proof using but no Section (#4124) | Enrico Tassi |
| 2015-03-11 | STM: ease re-editing of Admitted proofs | Enrico Tassi |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
