| Age | Commit message (Expand) | Author |
|---|
| 2015-10-09 | TQueue: Allow some tasks to be saved when clearing a TQueue | Alec Faithfull |
| 2015-10-09 | TQueue: Expose the length of TQueues | 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-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-08 | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-10-08 | Spawn: use each socket exclusively for writing or reading | 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-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-02 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-02 | Univs: fix semantics of Type in proof mode in universe-polymorphic mode | Matthieu Sozeau |
| 2015-10-02 | Univs: fix handling of side effects/delayed proofs | Matthieu Sozeau |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau |
| 2015-09-29 | Remove some uses of Loadpath.get_paths. | Guillaume Melquiond |
| 2015-09-26 | Hardening the API of evarmaps. | Pierre-Marie Pédrot |
| 2015-09-25 | Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua... | Arnaud Spiwack |
| 2015-09-20 | Rich printing of messages. | Pierre-Marie Pédrot |
| 2015-09-17 | Merge branch 'v8.5' into trunk | Maxime Dénès |
| 2015-09-15 | STM: Reset takes Ltac <ident> into account (Close #4316) | Enrico Tassi |
| 2015-09-14 | Univs: Add universe binding lists to definitions | Matthieu Sozeau |
| 2015-09-08 | More potentialities in proof_terminators. | Pierre-Marie Pédrot |
| 2015-09-08 | Opacifying the proof_terminator type. | Pierre-Marie Pédrot |
| 2015-09-01 | STM: save a full state for queries. | Enrico Tassi |
| 2015-08-19 | Removing code duplication in Lemmas. | Pierre-Marie Pédrot |
| 2015-08-19 | Documentation by giving a name to a large type. | Pierre-Marie Pédrot |
| 2015-08-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross |
| 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-26 | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" | Lionel Rieg |
| 2015-06-24 | Add corresponding field in `VernacInductive`. | Arnaud Spiwack |
| 2015-06-24 | Splitting the library representation on disk in two. | Pierre-Marie Pédrot |
| 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-06-03 | Admitted does not drop poly-univ constraints (Fix #4244) | Enrico Tassi |
| 2015-05-28 | STM: preserve branch name on edit (Close: #4245, #4246) | Enrico Tassi |
| 2015-05-27 | Fix bug #4159 | Matthieu Sozeau |
| 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 | Fix some typos. | Guillaume Melquiond |
| 2015-04-02 | CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168) | Enrico Tassi |
| 2015-03-27 | Putting the From parameter of the Require command into the AST. | Pierre-Marie Pédrot |
| 2015-03-27 | STM: refine the notion of "simply a tactic" | Enrico Tassi |
