| Age | Commit message (Expand) | Author |
|---|
| 2014-10-16 | Move the handling of the principal evar from refine to evd. | Arnaud Spiwack |
| 2014-10-16 | Move the handling a new evars from the [Proofview.Refine] module to [Evd]. | Arnaud Spiwack |
| 2014-10-16 | Evd: a few comments to document the increasingly wide internal [evar_map] type. | Arnaud Spiwack |
| 2014-10-16 | Evd: remove/update obsolete comments. | Arnaud Spiwack |
| 2014-10-15 | To stay closer to non-primitive projections, only unfold primitive | Matthieu Sozeau |
| 2014-10-15 | Make use of unfolded primitive projections when elaborating match on a | Matthieu Sozeau |
| 2014-10-15 | Fix bug 3637. | Matthieu Sozeau |
| 2014-10-15 | Reenable FO unification of primitive projections and their eta-expanded | Matthieu Sozeau |
| 2014-10-15 | Modify the heuristic for unfolding lhs or rhs in evarconv, considering | Matthieu Sozeau |
| 2014-10-15 | Implement a different strategy to expand primitive projections only when | Matthieu Sozeau |
| 2014-10-15 | Add an option to not print primitive projection parameters, which can | Matthieu Sozeau |
| 2014-10-14 | Oops, forgot a fix needed after the rebase. | Matthieu Sozeau |
| 2014-10-14 | Fix bug #3698: stack overflow due to eta+canonical structures in | Matthieu Sozeau |
| 2014-10-13 | Adding a tactic which fails if one of the goals under focus is dependent in a... | Hugo Herbelin |
| 2014-10-13 | Moving function about locs in locusops. | Hugo Herbelin |
| 2014-10-13 | English typo in a function name of evarconv. | Hugo Herbelin |
| 2014-10-13 | Added support for several impossible cases in compilation of "match". | Hugo Herbelin |
| 2014-10-12 | Tentative fix for a badly used Option.get in Reductionops. | Pierre-Marie Pédrot |
| 2014-10-11 | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name | Matthieu Sozeau |
| 2014-10-10 | Do not expand primitive projections eagerly in evarconv, but only | Matthieu Sozeau |
| 2014-10-10 | Add debug printers for projections, fix printing of evar constraints | Matthieu Sozeau |
| 2014-10-10 | Add a "Debug Tactic Unification" option and correct the first-order | Matthieu Sozeau |
| 2014-10-10 | Make constrMatching and detyping more robust with respect to | Matthieu Sozeau |
| 2014-10-10 | Fix bug due to shadowing a variable name in tacred | Matthieu Sozeau |
| 2014-10-08 | fix make mlidoc | Pierre Boutillier |
| 2014-10-08 | Fixing the anomaly in bug #3045 (a filter was not type-safe in | Hugo Herbelin |
| 2014-10-07 | Build unfolded versions of the primitive projection in let (a, p) := ... | Matthieu Sozeau |
| 2014-10-07 | Avoid a warning with Meta's names in debugger. | Hugo Herbelin |
| 2014-10-05 | A few improvements on pattern-matching compilation. | Hugo Herbelin |
| 2014-10-04 | A few Global.env removed. | Hugo Herbelin |
| 2014-10-03 | Fixing ennoying warning about evars named ?23 and so on. | Hugo Herbelin |
| 2014-10-03 | Fixing #3623 (unbound evars in types in a call to "change with"). | Hugo Herbelin |
| 2014-10-03 | Fixing #3634 (wrong env in "cannot instantiate because not in its | Hugo Herbelin |
| 2014-10-02 | Fixing interpretation of constr under binders which was broken after | Hugo Herbelin |
| 2014-10-02 | Completing fixing order of parameters when translating from | Hugo Herbelin |
| 2014-10-02 | Work around issues with FO unification trying to unify terms of | Matthieu Sozeau |
| 2014-10-02 | Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv. | Matthieu Sozeau |
| 2014-10-01 | Fix cbn behavior wrt simpl no match | Pierre Boutillier |
| 2014-10-01 | Fix the refolding by cbn of mutal constants defined in not included modules | Pierre Boutillier |
| 2014-10-01 | Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars | Hugo Herbelin |
| 2014-10-01 | Fixing use of arguments renaming in apply which was broken after | Hugo Herbelin |
| 2014-09-30 | Seeing IntroWildcard as an action intro pattern rather than as a naming pattern | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-30 | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau |
| 2014-09-29 | Merging some functions from evarutil.ml/evd.ml. | Hugo Herbelin |
| 2014-09-29 | Restoring non-uniform delta on local and global constants in 2nd order | Hugo Herbelin |
| 2014-09-29 | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-27 | Index keys instead of simply global references. | Matthieu Sozeau |
| 2014-09-27 | First version of keyed subterm selection in unification. | Matthieu Sozeau |
