| Age | Commit message (Expand) | Author |
|---|
| 2014-08-03 | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau |
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-07-21 | More straightforward definition of Universes.add_list_map. | Pierre-Marie Pédrot |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau |
| 2014-07-21 | Unifying locate code, also making it more powerful: it is now able to find | Pierre-Marie Pédrot |
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot |
| 2014-07-21 | More complete printing of Ltac location, akin to the term-dedicated Locate co... | Pierre-Marie Pédrot |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-06-25 | all coqide specific files moved into ide/ | Enrico Tassi |
| 2014-06-21 | When discharging polymorphic definitions, we must take into account all | Matthieu Sozeau |
| 2014-06-20 | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-17 | - Fix the de Bruijn problem in check_projection for good :) | Matthieu Sozeau |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-06-16 | Checking that a library name is valid before compilation. | Pierre-Marie Pédrot |
| 2014-06-13 | Deprecate options -dont, -lazy, -force-load-proofs. | Guillaume Melquiond |
| 2014-06-13 | Less ocaml warnings. | Hugo Herbelin |
| 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 | ind_tables: always declare side effects (Closes: HOTT#110) | Enrico Tassi |
| 2014-06-08 | Function in Univ uselessly exported. | Pierre-Marie Pédrot |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-22 | Fix native_compute for systems with a limited size for the command line. | Guillaume Melquiond |
| 2014-05-16 | Declare: fix Future management | Enrico Tassi |
| 2014-05-15 | heads: avoid forcing opaque proofs | Enrico Tassi |
| 2014-05-11 | Eliminating a potentially quadratic behaviour in Require, by using maps | Pierre-Marie Pédrot |
| 2014-05-06 | Fix extraction taking a type in the wrong environment. | Matthieu Sozeau |
| 2014-05-06 | Avoid u+k <= v constraints, don't take the sup of an algebraic universe during | Matthieu Sozeau |
| 2014-05-06 | - Add back some compatibility functions to avoid rewriting plugins. | Matthieu Sozeau |
| 2014-05-06 | - Fix arity handling in retyping (de Bruijn bug!) | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context removing some universes that do appear in the t... | Matthieu Sozeau |
| 2014-05-06 | Fix restrict_universe_context to not remove useful constraints. | 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 | Adapt Y. Bertot's path on private inductives (now the keyword is "Private"). | Yves Bertot |
| 2014-05-06 | - Fix abstract forgetting about new constraints. | Matthieu Sozeau |
| 2014-05-06 | - Fix handling of polymorphic inductive elimination schemes. | Matthieu Sozeau |
| 2014-05-06 | Fix printing of projections with implicits. | Matthieu Sozeau |
| 2014-05-06 | - Fix comparison of universes. | Matthieu Sozeau |
| 2014-05-06 | - Rename eq to equal in Univ, document new modules, set interfaces. | Matthieu Sozeau |
| 2014-05-06 | Fix interface for template polymorphism, cleaning up code in all typing algor... | 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-01 | Fixing ml-doc. | Pierre-Marie Pédrot |
