| Age | Commit message (Expand) | Author |
|---|
| 2015-05-27 | Fix bug #4159 | Matthieu Sozeau |
| 2015-03-22 | typo | Enrico Tassi |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-02-10 | Granting wish #4008. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu |
| 2015-01-05 | Added more informative messages about bullets. | Pierre Courtieu |
| 2014-12-28 | Call nf_constraints also when compiling directly to vo | Enrico Tassi |
| 2014-12-28 | Proof using: call "clear" to remove from sight the vars not selected | Enrico Tassi |
| 2014-12-27 | proof_global: make it possible to call close_proof in a worker | Enrico Tassi |
| 2014-12-26 | Call Evd.nf_constraints only on Univ Poly constants | Enrico Tassi |
| 2014-12-23 | Vi2vo: fix handling of univ constraints coming from the body | Enrico Tassi |
| 2014-11-09 | new: Optimize Proof, Optimize Heap | Enrico Tassi |
| 2014-11-01 | Add [Info] command. | Arnaud Spiwack |
| 2014-09-12 | Add syntax [id]: to apply tactic to goal named id. | Hugo Herbelin |
| 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 |
