| Commit message (Expand) | Author | Age |
... | |
* | A few Global.env removed. | Hugo Herbelin | 2014-10-04 |
* | 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-03 |
* | 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-02 |
* | 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-10-01 |
* | 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-30 |
* | 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-29 |
* | 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-27 |
* | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau | 2014-09-26 |
* | Fix incorrect assert false in detyping. | Matthieu Sozeau | 2014-09-25 |
* | 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 | 2014-09-24 |
* | Fix bug #3656. | Matthieu Sozeau | 2014-09-23 |
* | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau | 2014-09-19 |
* | Fixes in Ltac pattern-matching on primitive projections | Matthieu Sozeau | 2014-09-19 |
* | Use smart mapping in map_constr_with_binders_left_to_right. | Matthieu Sozeau | 2014-09-19 |
* | Fixing #3641 (loop in e_contextually, introduced in r16525). | Hugo Herbelin | 2014-09-19 |
* | Revert change of e_contextually as it needlessly expands all primitive | Matthieu Sozeau | 2014-09-19 |
* | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau | 2014-09-18 |
* | Fix debug printing with primitive projections. | Matthieu Sozeau | 2014-09-18 |
* | Do not try to match on a subterm that is not closed in find_subterm. | Matthieu Sozeau | 2014-09-18 |
* | For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ... | Hugo Herbelin | 2014-09-18 |
* | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier | 2014-09-18 |
* | 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-17 |
* | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | 2014-09-17 |
* | Add a "Hint Mode ref (+ | -)*" hint for setting a global mode | Matthieu Sozeau | 2014-09-15 |
* | Fix: when interpreting a identifier in pretying, use the Ltac identifier subs... | Arnaud Spiwack | 2014-09-15 |
* | Fix a bug in the naming of binders. | Arnaud Spiwack | 2014-09-15 |
* | Fix bug #3610, allowing betaiotadelta reduction while unifying types of | Matthieu Sozeau | 2014-09-15 |