| Commit message (Expand) | Author | Age |
|---|
| * | Add syntax [id]: to apply tactic to goal named id. |  Hugo Herbelin | 2014-09-12 |
| * | Simplify even further the declaration of primitive projections, |  Matthieu Sozeau | 2014-08-30 |
| * | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
| * | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | 2014-08-05 |
| * | STM: new "par:" goal selector, like "all:" but in parallel |  Enrico Tassi | 2014-08-05 |
| * | Making the error message about bullets more precise. |  Pierre Courtieu | 2014-07-31 |
| * | Fix handling of universes at the end of proofs, esp. for async proof processing. |  Matthieu Sozeau | 2014-07-25 |
| * | 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-23 |
| * | Feedback: LoadedFile + Goals | Enrico Tassi | 2014-07-11 |
| * | Force the final universe context of a proof only in poly || now case. | Matthieu Sozeau | 2014-06-24 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau | 2014-06-17 |
| * | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
| * | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau | 2014-05-16 |
| * | - 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-05-06 |
| * | 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-03-05 |
| * | STM: fix valid_id coming from Qed errors | Enrico Tassi | 2014-02-10 |
| * | Proof_global: Simpler API for proof_terminator | Enrico Tassi | 2014-01-04 |
| * | Qed: feedback when type checking is done | Enrico Tassi | 2013-12-24 |
| * | 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-12-04 |
| * | Allowing proofs starting with a non-empty evarmap. |  ppedrot | 2013-11-04 |
| * | 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-11-02 |
| * | Future: better doc + restore ~pure optimization |  gareuselesinge | 2013-10-31 |
| * | 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-18 |
| * | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |
| * | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
| * | safe Conv_oracle state for type checking | gareuselesinge | 2013-08-30 |
Hugo Herbelin
Matthieu Sozeau
Enrico Tassi
Pierre Courtieu
Matthieu Sozeau
Arnaud Spiwack
Pierre Letouzey
ppedrot
aspiwack
gareuselesinge