| Age | Commit message (Expand) | Author |
|---|
| 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-24 | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau |
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau |
| 2014-09-17 | Be more conservative and keep the use of eq_constr in pretyping/ functions. | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-15 | Fix bug #3610, allowing betaiotadelta reduction while unifying types of | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-11 | Fix bug #3505. | Matthieu Sozeau |
| 2014-09-10 | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin |
| 2014-09-04 | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-28 | Fix bugs #3484 and #3546. | Matthieu Sozeau |
| 2014-08-28 | Fixing an unnatural selection of subterms larger than expected in the | Hugo Herbelin |
| 2014-08-26 | Make evarconv and unification able to handle eta for records in presence | Matthieu Sozeau |
| 2014-08-26 | Fix compilation error due to commented code in previous commit by Hugo. | Matthieu Sozeau |
| 2014-08-25 | Fixing the essence of naming bug #3204: use same strategy for naming | Hugo Herbelin |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau |
| 2014-08-18 | Fixing unification of subterms identified by patterns. | Hugo Herbelin |
| 2014-08-18 | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau |
| 2014-08-14 | Remove confusing behavior of unify_with_subterm that could fail with | Matthieu Sozeau |
| 2014-08-09 | Do early occur-check in unification to allow eta to fire (fixes bug #3477) | Matthieu Sozeau |
| 2014-08-03 | - Fix has_undefined_evars not using its or_sorts argument anymore. | Matthieu Sozeau |
| 2014-07-09 | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau |
| 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-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-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-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-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-04 | - Allow parsing of @const@{instance} for specifying universe instances of pol... | Matthieu Sozeau |
| 2014-05-28 | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau |
| 2014-05-26 | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau |
| 2014-05-09 | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau |
| 2014-05-08 | Fix performance problem with unification in presence of universes (bug #3302)... | Matthieu Sozeau |
| 2014-05-06 | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau |
| 2014-05-06 | - Fix eq_constr_universes restricted to Sorts.equal | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | - Fix comparison of universes. | Matthieu Sozeau |
| 2014-05-06 | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-23 | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot |
| 2014-02-24 | Reductionops.Stack.strip* are ready to deal with Shift | Pierre Boutillier |
| 2014-02-24 | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier |
