| Commit message (Expand) | Author | Age |
|---|
| * | Keyed unification option, compiling the whole standard library |  Matthieu Sozeau | 2014-09-27 |
| * | Index keys instead of simply global references. | Matthieu Sozeau | 2014-09-27 |
| * | First version of keyed subterm selection in unification. | Matthieu Sozeau | 2014-09-27 |
| * | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
| * | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau | 2014-09-24 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. |  Hugo Herbelin | 2014-09-13 |
| * | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau | 2014-09-10 |
| * | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
| * | Removing dead code relative to the XML plugin. |  Pierre-Marie Pédrot | 2014-09-08 |
| * | Print [Variant] types with the keyword [Variant]. |  Arnaud Spiwack | 2014-09-04 |
| * | Fixing bug #2818. | Pierre-Marie Pédrot | 2014-09-03 |
| * | Fix Declaremods.end_library (Closes: #3536) |  Enrico Tassi | 2014-09-02 |
| * | 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 |
| * | Fix computation of dangling constraints at the end of a proof (bug #3531). | Matthieu Sozeau | 2014-08-25 |
| * | instanciation is French, instantiation is English |  Jason Gross | 2014-08-25 |
| * | Grammar: "avoiding to" isn't proper, either | Jason Gross | 2014-08-25 |
| * | Small code simplification. | Pierre-Marie Pédrot | 2014-08-05 |
| * | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
| * | - Do module substitution inside mind_record. |  Matthieu Sozeau | 2014-07-25 |
| * | 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-21 |
| * | Feedback: LoadedFile + Goals | Enrico Tassi | 2014-07-11 |
| * | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau | 2014-07-03 |
| * | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
| * | all coqide specific files moved into ide/ | Enrico Tassi | 2014-06-25 |
| * | When discharging polymorphic definitions, we must take into account all | Matthieu Sozeau | 2014-06-21 |
| * | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau | 2014-06-20 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | 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-17 |
| * | Checking that a library name is valid before compilation. | Pierre-Marie Pédrot | 2014-06-16 |
| * | Deprecate options -dont, -lazy, -force-load-proofs. |  Guillaume Melquiond | 2014-06-13 |
| * | Less ocaml warnings. | Hugo Herbelin | 2014-06-13 |
| * | - 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 |
| * | 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-08 |
| * | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | 2014-06-04 |
| * | Fix native_compute for systems with a limited size for the command line. | Guillaume Melquiond | 2014-05-22 |
| * | Declare: fix Future management | Enrico Tassi | 2014-05-16 |
| * | heads: avoid forcing opaque proofs | Enrico Tassi | 2014-05-15 |
| * | Eliminating a potentially quadratic behaviour in Require, by using maps | Pierre-Marie Pédrot | 2014-05-11 |
| * | 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 |
Matthieu Sozeau
Hugo Herbelin
Pierre-Marie Pédrot
Arnaud Spiwack
Enrico Tassi
Jason Gross
Matthieu Sozeau
Guillaume Melquiond