| Commit message (Expand) | Author | Age |
* | When building on-the-fly elimination principles, set the predicates universe ... | Matthieu Sozeau | 2014-06-29 |
* | Really honor the [simpl never] flag in whd_simpl, it was still doing reductio... | Matthieu Sozeau | 2014-06-29 |
* | Quick fix of bug #2996 continued (case of inductive types). | Hugo Herbelin | 2014-06-28 |
* | Quickly fixing bug #2996: typing functions now check when referring to | Hugo Herbelin | 2014-06-28 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Extra check for indirect dependency when abstracting a term which is | Hugo Herbelin | 2014-06-28 |
* | Made the subterm finding function make_abstraction independent of the | Hugo Herbelin | 2014-06-28 |
* | Small short optimization of instantiation in Evd. | Hugo Herbelin | 2014-06-28 |
* | Fast path in Canonical structure detection. We do not always compute the normal | Pierre-Marie Pédrot | 2014-06-27 |
* | Deactivate the "Standard Propositions Naming" flag, source of a lot of | Hugo Herbelin | 2014-06-26 |
* | Add an option to disable typeclass resolution during conversion, which | Matthieu Sozeau | 2014-06-26 |
* | Change interface of refresh universes to get a pbty argument instead of | Matthieu Sozeau | 2014-06-26 |
* | Use the right transparent state when comparing _types_ of metas. | Matthieu Sozeau | 2014-06-25 |
* | Fix type_of_inductive_knowing_conclusion, relying on an actually broken univ_... | Matthieu Sozeau | 2014-06-25 |
* | Use full transparent state when checking well-typedness of a second order mat... | Matthieu Sozeau | 2014-06-25 |
* | Fix program cases and inversion tactic to correctly record universe constraints. | Matthieu Sozeau | 2014-06-24 |
* | Fix for bug 1951, allowing at least fully-applied inductives types to be used | Matthieu Sozeau | 2014-06-23 |
* | - 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 |