| Commit message (Expand) | Author | Age |
* | Use kernel conversion on terms that contain universe variables during unifica... | Matthieu Sozeau | 2014-07-20 |
* | Fix coercion code to disallow using cumulativity in the domain of products, w... | Matthieu Sozeau | 2014-07-17 |
* | Add interface function to replace new_Type () | Matthieu Sozeau | 2014-07-14 |
* | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau | 2014-07-10 |
* | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau | 2014-07-09 |
* | 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-07 |
* | 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-03 |
* | Fix a Not_found anomaly raised by solve_evar_evar, we were breaking the | Matthieu Sozeau | 2014-07-02 |
* | Add toplevel commands to declare global universes and constraints. | Matthieu Sozeau | 2014-07-01 |
* | Clarifying 'No such bound variable' message in apply, as suggested in #2387 | Hugo Herbelin | 2014-06-30 |
* | 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 |