aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Fix spacing in error message.Gravatar Guillaume Melquiond2014-06-16
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
* Remove documentation for the unsupported options -byte and -opt.Gravatar Guillaume Melquiond2014-06-13
* Deprecate useless option -unsafe.Gravatar Guillaume Melquiond2014-06-13
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
* Improved error message when a meta posed as an evar remains unsolvedGravatar Hugo Herbelin2014-06-13
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* - Fix substitution of universes which needlessly hashconsed existing universes.Gravatar Matthieu Sozeau2014-06-10
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
* Adding a toplevel option allowing to deactivate the term sharing in kernelGravatar Pierre-Marie Pédrot2014-06-08
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* ind_tables: always declare side effects (Closes: HOTT#110)Gravatar Enrico Tassi2014-06-08
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
* Remove the syntax [Vernac1. Vernac2. … Vernacn. ].Gravatar Arnaud Spiwack2014-06-06
* Collecting in Namegen those conventional default names that are used in diffe...Gravatar Hugo Herbelin2014-06-04
* - Allow parsing of @const@{instance} for specifying universe instances of pol...Gravatar Matthieu Sozeau2014-06-04
* - Force every universe level to be >= Prop, so one cannot "go under" it anymore.Gravatar Matthieu Sozeau2014-06-04
* Fix handling of anonymous Type in template universe polymorphic inductivesGravatar Matthieu Sozeau2014-06-04
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* More fixes of unification with primitive projections (missed cases during the...Gravatar Matthieu Sozeau2014-05-16
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Fix the behaviour of ML tactic notations w.r.t. Imports by making themGravatar Pierre-Marie Pédrot2014-05-13
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Adding the possibility for ML modules to declare functions to be called atGravatar Pierre-Marie Pédrot2014-05-12
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* Cleanup before merge with the trunkGravatar Matthieu Sozeau2014-05-06
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Proper calculation of constructor levels, forgetting the level of lets.Gravatar Matthieu Sozeau2014-05-06
* Retype application of fix_proto to get the right universes in ProgramGravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* Fix declarations of monomorphic assumptionsGravatar Matthieu Sozeau2014-05-06
* Allow records whose sort is defined by a constant.Gravatar Matthieu Sozeau2014-05-06
* - Fix RecTutorial, and mutual induction schemes getting the wrong names.Gravatar Matthieu Sozeau2014-05-06
* Fix program Fixpoint not taking care of universes.Gravatar Matthieu Sozeau2014-05-06
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix context forgetting universes (temporary, the fix is not exactly right).Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* Various fixes of universe polymorphism and projections when they're set.Gravatar Matthieu Sozeau2014-05-06
* - Fix Check to use the constraints inferred during type inference.Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 00:54:54 +0000