| Commit message (Expand) | Author | Age |
|---|
| * | Remove some uses of Loadpath.get_paths. |  Guillaume Melquiond | 2015-09-29 |
| * | STM: Reset takes Ltac <ident> into account (Close #4316) |  Enrico Tassi | 2015-09-15 |
| * | Univs: Add universe binding lists to definitions |  Matthieu Sozeau | 2015-09-14 |
| * | STM: save a full state for queries. | Enrico Tassi | 2015-09-01 |
| * | 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-19 |
| * | 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-30 |
| * | Fixing what seems to be a typo. |  Hugo Herbelin | 2015-07-29 |
| * | ShowScript: as 8.4 w.r.t. unnamed proofs and non tactic vernacs (fix #4308) | Enrico Tassi | 2015-07-28 |
| * | STM: fix a "exn with no safe id attached" error on a failing query | Enrico Tassi | 2015-07-14 |
| * | Introduction of a "Undelimit Scope" command, undoing "Delimit Scope" |  Lionel Rieg | 2015-06-26 |
| * | Splitting the library representation on disk in two. | Pierre-Marie Pédrot | 2015-06-24 |
| * | 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-09 |
| * | Admitted does not drop poly-univ constraints (Fix #4244) | Enrico Tassi | 2015-06-03 |
| * | STM: preserve branch name on edit (Close: #4245, #4246) | Enrico Tassi | 2015-05-28 |
| * | Fix bug #4159 |  Matthieu Sozeau | 2015-05-27 |
| * | nice error for Restart outside a proof (Close: #4235) | Enrico Tassi | 2015-05-12 |
| * | Add a [Redirect] vernacular command |  Clément Pit--Claudel | 2015-05-04 |
| * | STM: print trace on "anomaly, no safe id attached" | Enrico Tassi | 2015-04-21 |
| * | Fix some typos. | Guillaume Melquiond | 2015-04-02 |
| * | CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168) | Enrico Tassi | 2015-04-02 |
| * | 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 | 2015-03-27 |
| * | STM: change how proof mode switching commands are handled (decl_mode) | Enrico Tassi | 2015-03-26 |
| * | STM: avoid processing asynchronously empty proofs (Close: #4134) | Enrico Tassi | 2015-03-25 |
| * | 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-22 |
| * | Fixed #4138. In emacs mode Set/Unset does not print the goal anymore. |  Pierre Courtieu | 2015-03-20 |
| * | 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-15 |
| * | Fixing bug #4055. | Pierre-Marie Pédrot | 2015-03-12 |
| * | 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 | 2015-03-11 |
| * | STM: Considering Stack_overflow as a normal tactic error (Close #3576) | Enrico Tassi | 2015-02-27 |
| * | STM: proof state also includes meta counters | Enrico Tassi | 2015-02-25 |
| * | Future: human readable name for delegated (Close #4065) | Enrico Tassi | 2015-02-21 |
| * | STM: when async_proofs_full is set process only tasks in the perspective | Enrico Tassi | 2015-02-16 |
| * | *Queue: API to wake up all threads | Enrico Tassi | 2015-02-16 |
| * | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi | 2015-02-15 |
| * | Reset "section name" works again (Close #3933) | Enrico Tassi | 2015-02-15 |
| * | Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior | Enrico Tassi | 2015-02-14 |
| * | STM: is Flags.async_proofs_full then always delegate | Enrico Tassi | 2015-02-11 |
| * | Improving further e11854569b8 and 3e5b9ab9f75e4 on when to print goals in coq... | Hugo Herbelin | 2015-02-10 |
| * | Fix bug #4014. | Pierre-Marie Pédrot | 2015-02-09 |
| * | STM: tolerate simple side effects in async proofs (Close: 4006) | Enrico Tassi | 2015-02-07 |
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Lionel Rieg
Matthieu Sozeau
Clément Pit--Claudel
Pierre Courtieu