| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Fix bug #3621, using fold_left2 on arrays of the same size only. | Matthieu Sozeau | 2014-09-15 |
| * | Rework typeclass resolution and control of backtracking. | Matthieu Sozeau | 2014-09-15 |
| * | Using "Evd.restrict" in tactic clear so as to keep evar names. | Hugo Herbelin | 2014-09-13 |
| * | Exporting apply_subfilter from Evd.ml. | Hugo Herbelin | 2014-09-13 |
| * | Fixing synchronization of evar names table when merging evar_map. | Hugo Herbelin | 2014-09-13 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
| * | Checking typability of evar instances. Using ";" to separate bindings | Hugo Herbelin | 2014-09-13 |
| * | An old typo which was preventing example #3537 to work the same as it | Hugo Herbelin | 2014-09-12 |
| * | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | 2014-09-12 |
| * | Parsing evar instances. | Hugo Herbelin | 2014-09-12 |
| * | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | 2014-09-12 |
| * | Add a flag for restricting resolution of typeclasses to |  Matthieu Sozeau | 2014-09-11 |
| * | Fix bug #3594: eta for constructors and functions at the same time which | Matthieu Sozeau | 2014-09-11 |
| * | Fix bug #3596, wrong treatment of projections in compute_constelim_direct. | Matthieu Sozeau | 2014-09-11 |
| * | Fix bug #3505. | Matthieu Sozeau | 2014-09-11 |
| * | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin | 2014-09-10 |
| * | Fix generation of inductive elimination principle for primitive records. | Matthieu Sozeau | 2014-09-10 |
| * | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau | 2014-09-09 |
| * | Parsing of Type@{max(i,j)}. | Matthieu Sozeau | 2014-09-08 |
Matthieu Sozeau
Hugo Herbelin
Pierre Boutillier
Arnaud Spiwack
Matthieu Sozeau