| Age | Commit message (Expand) | Author |
|---|
| 2014-07-29 | Fix bug #3453, not recognizing primitive projections in Coercion declarations. | Matthieu Sozeau |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau |
| 2014-07-17 | Fix coercion code to disallow using cumulativity in the domain of products, w... | Matthieu Sozeau |
| 2014-07-14 | Add interface function to replace new_Type () | Matthieu Sozeau |
| 2014-07-10 | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau |
| 2014-07-09 | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau |
| 2014-07-07 | In flex-flex cases, the undefinedness of an evar can not be preseved after co... | Matthieu Sozeau |
| 2014-07-07 | Missing check of evar instantiation, resulting in missing constraints (bug fr... | Matthieu Sozeau |
| 2014-07-03 | Cleanup code related to the constraint solving, which sits now outside the | Matthieu Sozeau |
| 2014-07-03 | Fix eta expansion of primitive records (HoTT bug #78), which now fails cleanl... | Matthieu Sozeau |
| 2014-07-03 | When defining a monomorphic Program, do not allow arbitrary instantiations | Matthieu Sozeau |
| 2014-07-02 | Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the | Matthieu Sozeau |
| 2014-07-01 | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau |
| 2014-06-30 | Clarifying 'No such bound variable' message in apply, as suggested in #2387 | Hugo Herbelin |
| 2014-06-29 | 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-28 | 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-27 | Fast path in Canonical structure detection. We do not always compute the normal | Pierre-Marie Pédrot |
| 2014-06-26 | 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-25 | 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-24 | Fix program cases and inversion tactic to correctly record universe constraints. | Matthieu Sozeau |
| 2014-06-23 | Fix for bug 1951, allowing at least fully-applied inductives types to be used | Matthieu Sozeau |
| 2014-06-21 | - Add an option to refresh only algebraic universes, for e_type_of. The goal | Matthieu Sozeau |
| 2014-06-20 | 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-19 | - Fix bug in unification, not only named metas are turned into evars (e.g. in... | Matthieu Sozeau |
| 2014-06-18 | 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-17 | 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-16 | 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-15 | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau |
| 2014-06-13 | 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 |
