| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-02-12 | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-29 | Optimization in unification: when checking that the head of a term is an | ppedrot |
| 2013-10-29 | Useless array-to-list casts in Unification. | ppedrot |
| 2013-10-29 | Do not generate useless argument arrays in whd_* functions. | ppedrot |
| 2013-10-29 | - install evar printer for debugging | msozeau |
| 2013-10-23 | cList: set-as-list functions are now with an explicit comparison | letouzey |
| 2013-10-23 | Small optimizations in unification. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-07-19 | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau |
| 2013-06-19 | - Keep the refinement of existing evars comming from unification with a rewri... | msozeau |
| 2013-05-10 | Little oversight in commit r16489 (fix for bug #3036). | herbelin |
| 2013-05-08 | Protection against "Bad recursive type" in w_unify0 (bug #3036). | herbelin |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-25 | Fix bug #2989: make unification.ml able to deal with canonical structure in a... | pboutill |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey |
| 2013-02-25 | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... | pboutill |
| 2013-02-17 | A more informative message when the elimination predicate for | herbelin |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-02-10 | Splitted Evarutil in two files | ppedrot |
| 2013-02-05 | Revert "Ordered evars by level of dependency in the merging phase of unificat... | herbelin |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-27 | Ordered evars by level of dependency in the merging phase of unification | herbelin |
