| Commit message (Expand) | Author | Age |
* | Revert patch making the oracle be used for the transparent state in evarconv, | Matthieu Sozeau | 2014-07-09 |
* | 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 |
* | 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 |
* | 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 |
* | 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 |
* | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
* | - Allow parsing of @const@{instance} for specifying universe instances of pol... | Matthieu Sozeau | 2014-06-04 |
* | - Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some | Matthieu Sozeau | 2014-05-28 |
* | - Fix in kernel conversion not folding the universe constraints | Matthieu Sozeau | 2014-05-26 |
* | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau | 2014-05-09 |
* | Fix performance problem with unification in presence of universes (bug #3302)... | Matthieu Sozeau | 2014-05-08 |
* | - 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-05-06 |
* | Removing dead code, thanks to new OCaml warnings and a bit of scripting. | Pierre-Marie Pédrot | 2014-04-23 |
* | 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-24 |
* | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi | 2014-02-12 |
* | Conv_orable made functional and part of pre_env | gareuselesinge | 2013-10-31 |
* | 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-29 |
* | cList: set-as-list functions are now with an explicit comparison | letouzey | 2013-10-23 |
* | Small optimizations in unification. | ppedrot | 2013-10-23 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
* | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau | 2013-07-19 |
* | - Keep the refinement of existing evars comming from unification with a rewri... | msozeau | 2013-06-19 |
* | Little oversight in commit r16489 (fix for bug #3036). | herbelin | 2013-05-10 |
* | Protection against "Bad recursive type" in w_unify0 (bug #3036). | herbelin | 2013-05-08 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Fix bug #2989: make unification.ml able to deal with canonical structure in a... | pboutill | 2013-03-25 |
* | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey | 2013-03-13 |
* | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... | pboutill | 2013-02-25 |
* | 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-17 |
* | Splitted Evarutil in two files | ppedrot | 2013-02-10 |
* | Revert "Ordered evars by level of dependency in the merging phase of unificat... | herbelin | 2013-02-05 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Ordered evars by level of dependency in the merging phase of unification | herbelin | 2013-01-27 |
* | Fixed a little inefficiency of "set/destruct" over a pattern. Now | herbelin | 2012-12-18 |