| Commit message (Expand) | Author | Age |
|---|
| * | - Add an option to refresh only algebraic universes, for e_type_of. The goal |  Matthieu Sozeau | 2014-06-21 |
| * | Fixed some HoTT bugs, provide a proper error message when giving an ill-formed | Matthieu Sozeau | 2014-06-20 |
| * | Cleanup treatment of template universe polymorphism (thanks to E. Tassi | Matthieu Sozeau | 2014-06-20 |
| * | - Fix bug in unification, not only named metas are turned into evars (e.g. in... | Matthieu Sozeau | 2014-06-19 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | Code factorization in LMap. |  Pierre-Marie Pédrot | 2014-06-18 |
| * | Reinstate eta for records in evarconv, fixing two HoTT coq bugs. | Matthieu Sozeau | 2014-06-17 |
| * | Adapt coercion code to work with projections as target classes. | Matthieu Sozeau | 2014-06-17 |
| * | Fixing #3282 (two bugs in the presence of let-in's in "fix"). |  Hugo Herbelin | 2014-06-17 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| * | Fix type inference of the record argument of a projection to catch ill-typed | Matthieu Sozeau | 2014-06-17 |
| * | - Fix the de Bruijn problem in check_projection for good :) | Matthieu Sozeau | 2014-06-17 |
| * | Existing Class now works with universe polymorphism. Fixes HoTT bug #063 | Matthieu Sozeau | 2014-06-17 |
| * | Unification in HoTT_coq_061.v was looping with previous commit (while | Hugo Herbelin | 2014-06-16 |
| * | Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation, | Hugo Herbelin | 2014-06-16 |
| * | - Add "Show Universes" to print information about universes during a proof. | Matthieu Sozeau | 2014-06-16 |
| * | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau | 2014-06-15 |
| * | Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of... | Matthieu Sozeau | 2014-06-13 |
| * | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin | 2014-06-13 |
| * | Improved error message when a meta posed as an evar remains unsolved | Hugo Herbelin | 2014-06-13 |
| * | Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284). | Hugo Herbelin | 2014-06-13 |
| * | Adapt simpl/cbn unfolding and refolding machinery to projections, so that | Matthieu Sozeau | 2014-06-13 |
| * | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau | 2014-06-11 |
| * | In generalized rewrite, avoid retyping completely and constantly the conclusi... | Matthieu Sozeau | 2014-06-11 |
| * | Compute the trace of a universe inconsistency only when explicitly required | Pierre-Marie Pédrot | 2014-06-10 |
| * | Made explanations for universe inconsistencies optional. They are only used | Pierre-Marie Pédrot | 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-10 |
| * | Fix canonical structure resolution in unification (bug found in Ssreflect). | Matthieu Sozeau | 2014-06-08 |
| * | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
| * | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin | 2014-06-04 |
| * | Fix canonical structure resolution (makes test-suite files go through again). | Matthieu Sozeau | 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 hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau | 2014-06-04 |
| * | - Keep all <= constraints during refinement, otherwise we might miss collapse... | Matthieu Sozeau | 2014-06-04 |
| * | cbn understand ! Arguments directive |  Pierre Boutillier | 2014-06-04 |
| * | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin | 2014-06-01 |
| * | Dead code + typo. | Hugo Herbelin | 2014-05-31 |
| * | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau | 2014-05-28 |
| * | Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q | Pierre Boutillier | 2014-05-26 |
| * | Reduction.Stack.Fix/Case stores Cst_stack.t | Pierre Boutillier | 2014-05-26 |
| * | Cst_stack before stack (abstraction leak in whd_gen) | Pierre Boutillier | 2014-05-26 |
| * | cbn: args list instead of arg number | Pierre Boutillier | 2014-05-26 |
| * | Reductionops.Stack.map & Reduction.iterate_whd_gen | Pierre | 2014-05-26 |
| * | - 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 |
| * | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau | 2014-05-16 |
| * | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau | 2014-05-09 |
| * | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau | 2014-05-09 |
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Pierre Boutillier