| Age | Commit message (Expand) | Author |
|---|
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-03 | Properly compute the transitive closure of the system of constraints | Matthieu Sozeau |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-07-01 | Making code and doc agree on "Set Equality Schemes" (see also bug #2550). | Hugo Herbelin |
| 2014-07-01 | Fixing the place where to insert a space in "Tactic failure" | Hugo Herbelin |
| 2014-07-01 | More informative message when Mltop.load_object fails. | Hugo Herbelin |
| 2014-06-30 | Useless keeping of dirpath in tactic aliases. | Pierre-Marie Pédrot |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-28 | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
| 2014-06-25 | cut toploop(s) out of coqtop: now they are loaded dynamically | Enrico Tassi |
| 2014-06-24 | Fix computation of Type argument for Program's fix_proto. | Matthieu Sozeau |
| 2014-06-23 | Proper handling of the polymorphism flag for Context, fixing HoTT bug #98. | Matthieu Sozeau |
| 2014-06-20 | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Adapt coercion code to work with projections as target classes. | Matthieu Sozeau |
| 2014-06-17 | Complying an ocaml warning. | Hugo Herbelin |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-06-16 | - 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-13 | 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-11 | Fix bug #3289 | Matthieu Sozeau |
| 2014-06-10 | - 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-08 | 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-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
| 2014-06-06 | Remove the syntax [Vernac1. Vernac2. … Vernacn. ]. | Arnaud Spiwack |
| 2014-06-04 | 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-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-16 | More fixes of unification with primitive projections (missed cases during the... | Matthieu Sozeau |
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi |
| 2014-05-13 | Fix the behaviour of ML tactic notations w.r.t. Imports by making them | Pierre-Marie Pédrot |
| 2014-05-12 | 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-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin |
| 2014-05-06 | 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 |
