| Age | Commit message (Expand) | Author |
|---|
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-07-31 | Making the error message about bullets more precise. | Pierre Courtieu |
| 2014-07-25 | Fix handling of universes at the end of proofs, esp. for async proof processing. | Matthieu Sozeau |
| 2014-07-23 | When closing a proof, make sure that the types have their evar substituted. | Arnaud Spiwack |
| 2014-07-23 | Proof_global: an unused variable replaced by a wildcard. | Arnaud Spiwack |
| 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-24 | Force the final universe context of a proof only in poly || now case. | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-16 | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau |
| 2014-05-06 | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Adapt universe polymorphic branch to new handling of futures for delayed proofs. | Matthieu Sozeau |
| 2014-05-06 | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau |
| 2014-05-06 | - Fix index-list to show computational relations for rewriting files. | 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-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-02-10 | STM: fix valid_id coming from Qed errors | Enrico Tassi |
| 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-04 | Allowing proofs starting with a non-empty evarmap. | ppedrot |
| 2013-11-02 | Adds a tactic give_up. | aspiwack |
| 2013-11-02 | Adds a shelve tactic. | aspiwack |
| 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-31 | Future: better doc + restore ~pure optimization | gareuselesinge |
| 2013-10-18 | proof modes: use ephemerons to represent them in proof state | gareuselesinge |
| 2013-10-18 | declaration_hooks use Ephemeron | gareuselesinge |
| 2013-10-18 | Future: ported to Ephemeron + exception enhancing | gareuselesinge |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-08-30 | safe Conv_oracle state for type checking | gareuselesinge |
| 2013-08-08 | stm: (initial) support for -coq-slaves | gareuselesinge |
