| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-09-27 | Fix bug #3664 by refolding projections that don't reduce in cbn. | Matthieu Sozeau |
| 2014-09-27 | Fix semantics of matching with folded/unfolded projections to definitely | Matthieu Sozeau |
| 2014-09-27 | Fix bug #3672, application of primitive projections as coercions. | Matthieu Sozeau |
| 2014-09-27 | Fix bug 3662 by actually reducing primitive projections in cbv/compute. | Matthieu Sozeau |
| 2014-09-27 | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-26 | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau |
| 2014-09-25 | Fix incorrect assert false in detyping. | Matthieu Sozeau |
| 2014-09-24 | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau |
| 2014-09-24 | Return a Prop not an arbitrary Type, and correct a typo. | Matthieu Sozeau |
| 2014-09-24 | Make eq_pattern_test/eq_test work up to the equivalence of primitive | Matthieu Sozeau |
