| Commit message (Expand) | Author | Age |
* | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau | 2014-06-16 |
* | Fix spacing in error message. | Guillaume Melquiond | 2014-06-16 |
* | Deprecate useless option -quality. | Guillaume Melquiond | 2014-06-13 |
* | Remove documentation for the unsupported options -byte and -opt. | Guillaume Melquiond | 2014-06-13 |
* | Deprecate useless option -unsafe. | Guillaume Melquiond | 2014-06-13 |
* | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond | 2014-06-13 |
* | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin | 2014-06-13 |
* | Fix bug #3289 | Matthieu Sozeau | 2014-06-11 |
* | - Fix substitution of universes which needlessly hashconsed existing universes. | Matthieu Sozeau | 2014-06-10 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | Adding a toplevel option allowing to deactivate the term sharing in kernel | Pierre-Marie Pédrot | 2014-06-08 |
* | Moving hook code from Future to Lemmas. This seemed to disrupt compilation of | Pierre-Marie Pédrot | 2014-06-08 |
* | Enforce a correct exception handling in declaration_hooks | Enrico Tassi | 2014-06-08 |
* | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi | 2014-06-08 |
* | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
* | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack | 2014-06-06 |
* | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
* | - Allow parsing of @const@{instance} for specifying universe instances of pol... | Matthieu Sozeau | 2014-06-04 |
* | - Force every universe level to be >= Prop, so one cannot "go under" it anymore. | Matthieu Sozeau | 2014-06-04 |
* | Fix handling of anonymous Type in template universe polymorphic inductives | Matthieu Sozeau | 2014-06-04 |
* | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
* | More fixes of unification with primitive projections (missed cases during the... | Matthieu Sozeau | 2014-05-16 |
* | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi | 2014-05-15 |
* | Fix the behaviour of ML tactic notations w.r.t. Imports by making them | Pierre-Marie Pédrot | 2014-05-13 |
* | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | 2014-05-12 |
* | Adding the possibility for ML modules to declare functions to be called at | Pierre-Marie Pédrot | 2014-05-12 |
* | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin | 2014-05-08 |
* | Cleanup before merge with the trunk | Matthieu Sozeau | 2014-05-06 |
* | - Fix treatment of global universe constraints which should be passed along | Matthieu Sozeau | 2014-05-06 |
* | Proper calculation of constructor levels, forgetting the level of lets. | Matthieu Sozeau | 2014-05-06 |
* | Retype application of fix_proto to get the right universes in Program | Matthieu Sozeau | 2014-05-06 |
* | Fix restrict_universe_context removing some universes that do appear in the t... | Matthieu Sozeau | 2014-05-06 |
* | Fix declarations of monomorphic assumptions | Matthieu Sozeau | 2014-05-06 |
* | Allow records whose sort is defined by a constant. | Matthieu Sozeau | 2014-05-06 |
* | - Fix RecTutorial, and mutual induction schemes getting the wrong names. | Matthieu Sozeau | 2014-05-06 |
* | Fix program Fixpoint not taking care of universes. | 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 context forgetting universes (temporary, the fix is not exactly right). | Matthieu Sozeau | 2014-05-06 |
* | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot | 2014-05-06 |
* | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau | 2014-05-06 |
* | Various fixes of universe polymorphism and projections when they're set. | Matthieu Sozeau | 2014-05-06 |
* | - Fix Check to use the constraints inferred during type inference. | Matthieu Sozeau | 2014-05-06 |
* | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau | 2014-05-06 |
* | Initial work on reintroducing old-style polymorphism for compatibility (the s... | 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 |
* | Allowing the "Declare Instance" command anywhere. This was artificially | Pierre-Marie Pédrot | 2014-05-01 |