| Age | Commit message (Expand) | Author |
|---|
| 2016-10-09 | A tentative fix for #5102 (bullets parsing broken by calls to parse_entry). | Hugo Herbelin |
| 2016-09-05 | Fix #5065: Anomaly: Not a proof by induction | Maxime Dénès |
| 2016-08-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot |
| 2016-08-30 | Fix #4871 - interrupting par:abstract kills coqtop | Maxime Dénès |
| 2016-06-14 | Admitted: fix #4818 return initial stmt and univs | Matthieu Sozeau |
| 2016-05-27 | STM: fix argument filtering for slaves | Enrico Tassi |
| 2016-05-26 | Pfedit.get_current_context refinement (fix #4523) | Matthieu Sozeau |
| 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-03-25 | Univs: fix get_current_context (bug #4603, part I) | Matthieu Sozeau |
| 2016-03-15 | Tentative fix for bug #4614: "Fully check the document" is uninterruptable. | Pierre-Marie Pédrot |
| 2016-03-04 | Rename Ephemeron -> CEphemeron. | 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 |
| 2016-01-04 | workers: purge short version of -load-vernac too (fix #4458) | Enrico Tassi |
| 2015-12-01 | vio: fix argument parsing (progress on #4442) | Enrico Tassi |
| 2015-11-28 | Univs: correctly register universe binders for lemmas. | Matthieu Sozeau |
| 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-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin |
| 2015-10-14 | When typechecking a lemma statement, try to resolve typeclasses before | Matthieu Sozeau |
| 2015-10-09 | STM: Work around an occasional crash in dot (debug output) | Alec Faithfull |
| 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-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 | 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-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-01 | STM: save a full state for queries. | Enrico Tassi |
| 2015-08-19 | Removing code duplication in Lemmas. | Pierre-Marie Pédrot |
