| Age | Commit message (Expand) | Author |
|---|
| 2016-05-10 | Proof_global, STM: cleanup + use default_proof_mode instead of "Classic" | Enrico Tassi |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-02 | Use streams rather than strings to handle bullet suggestions. | Guillaume Melquiond |
| 2015-11-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-11-28 | Univs: correctly register universe binders for lemmas. | Matthieu Sozeau |
| 2015-10-30 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-29 | Handle side-effects of Vernacular commands inside proofs better, so that | Matthieu Sozeau |
| 2015-10-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-28 | Avoid type checking private_constants (side_eff) again during Qed (#4357). | Enrico Tassi |
| 2015-10-19 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-18 | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin |
| 2015-10-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-09-08 | Opacifying the proof_terminator type. | Pierre-Marie Pédrot |
| 2015-07-29 | Fixing what seems to be a typo. | Hugo Herbelin |
| 2015-06-09 | STM: states coming from workers have no proof terminators (Close #4246) | Enrico Tassi |
| 2015-06-03 | Admitted does not drop poly-univ constraints (Fix #4244) | Enrico Tassi |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu |
| 2014-12-28 | Proof using: call "clear" to remove from sight the vars not selected | Enrico Tassi |
| 2014-12-23 | Vi2vo: fix handling of univ constraints coming from the body | Enrico Tassi |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-11-09 | new: Optimize Proof, Optimize Heap | Enrico Tassi |
| 2014-11-01 | Add [Info] command. | Arnaud Spiwack |
| 2014-07-25 | Fix handling of universes at the end of proofs, esp. for async proof processing. | Matthieu Sozeau |
| 2014-07-23 | Proof_global.start_dependent_proof: properly threads the sigma through the te... | Arnaud Spiwack |
| 2014-07-23 | Change the interface of proof_global to take an evar_map instead of a univers... | Arnaud Spiwack |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | Correct rebase on STM code. Thanks to E. Tassi for help on dealing with | Matthieu Sozeau |
| 2014-05-06 | Rework handling of universes on top of the STM, allowing for delayed | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-05 | Remove some dead-code (thanks to ocaml warnings) | Pierre Letouzey |
| 2014-01-04 | Proof_global: Simpler API for proof_terminator | Enrico Tassi |
| 2013-12-24 | Qed: feedback when type checking is done | Enrico Tassi |
| 2013-12-04 | Fix Admitted. | Arnaud Spiwack |
| 2013-12-04 | Proof_global: fix start_proof comment after the preceding commits. | Arnaud Spiwack |
| 2013-12-04 | Factoring(continued). | Arnaud Spiwack |
| 2013-12-04 | Refactoring: storing more information in the terminator closure. | Arnaud Spiwack |
| 2013-12-04 | The commands that initiate proofs are now in charge of what happens when proo... | Arnaud Spiwack |
| 2013-12-04 | Allow proofs to start with dependent goals. | Arnaud Spiwack |
| 2013-11-02 | New option Default Goal Selector. | aspiwack |
| 2013-11-02 | The tactic [admit] exits with the "unsafe" status. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-18 | declaration_hooks use Ephemeron | gareuselesinge |
| 2013-10-18 | Future: ported to Ephemeron + exception enhancing | gareuselesinge |
| 2013-08-08 | stm: (initial) support for -coq-slaves | gareuselesinge |
