| Commit message (Expand) | Author | Age |
* | 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 |
* | Fix bug #3589, unification looping due to incorrect use of stack with primiti... | Matthieu Sozeau | 2014-09-08 |
* | Fix bug #3584, elaborating pattern-matching on primitive records to the | Matthieu Sozeau | 2014-09-06 |
* | Cleanup code for looking up projection bodies. | Matthieu Sozeau | 2014-09-06 |
* | The pretyping of [uconstr] in [refine] uses the identifier of the ltac contex... | Arnaud Spiwack | 2014-09-05 |
* | Adds an identifier context in pretying's Ltac context. | Arnaud Spiwack | 2014-09-05 |
* | Proofview refiner is now type-safe by default. | Pierre-Marie Pédrot | 2014-09-04 |
* | Typing.sort_of does not leak evarmaps anymore. | Pierre-Marie Pédrot | 2014-09-04 |
* | Fix bug #3561, correct folding of env in context[] matching. | Matthieu Sozeau | 2014-09-04 |
* | Fix bug #3559, ensuring a canonical order of universe level quantifications when | Matthieu Sozeau | 2014-09-04 |
* | Print [Variant] types with the keyword [Variant]. | Arnaud Spiwack | 2014-09-04 |
* | Add test-suite file for Case derivation on primitive records. | Matthieu Sozeau | 2014-09-04 |
* | Fix bug #3563, making syntactic matching of primitive projections | Matthieu Sozeau | 2014-09-04 |
* | Fixing bug #3136. | Pierre-Marie Pédrot | 2014-09-02 |
* | In evarconv, do first-order unification of LetIn's properly, ensuring we comp... | Matthieu Sozeau | 2014-09-01 |
* | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
* | Fix bugs #3484 and #3546. | Matthieu Sozeau | 2014-08-28 |
* | There are some occurs-check cases that can be handled by imitation (using pru... | Matthieu Sozeau | 2014-08-28 |
* | Fixing an unnatural selection of subterms larger than expected in the | Hugo Herbelin | 2014-08-28 |
* | Debug RAKAM | Pierre Boutillier | 2014-08-26 |
* | Make evarconv and unification able to handle eta for records in presence | Matthieu Sozeau | 2014-08-26 |
* | Fix compilation error due to commented code in previous commit by Hugo. | Matthieu Sozeau | 2014-08-26 |
* | Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible | Matthieu Sozeau | 2014-08-25 |