| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Fixing the essence of naming bug #3204: use same strategy for naming | Hugo Herbelin | 2014-08-25 |
| * | instanciation is French, instantiation is English |  Jason Gross | 2014-08-25 |
| * | Grammar: "avoiding to" isn't proper, either | Jason Gross | 2014-08-25 |
| * | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau | 2014-08-22 |
| * | Fixing unification of subterms identified by patterns. | Hugo Herbelin | 2014-08-18 |
| * | Refine patch for behavior of unify_to_subterm to allow backtracking on | Matthieu Sozeau | 2014-08-18 |
| * | Remove confusing behavior of unify_with_subterm that could fail with | Matthieu Sozeau | 2014-08-14 |
| * | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau | 2014-08-14 |
| * | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | 2014-08-14 |
| * | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau | 2014-08-13 |
| * | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau | 2014-08-10 |
| * | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | 2014-08-09 |
| * | Allow pattern matching on the applied form of projections with primitive | Matthieu Sozeau | 2014-08-09 |
| * | Do early occur-check in unification to allow eta to fire (fixes bug #3477) | Matthieu Sozeau | 2014-08-09 |
| * | Using the asymmetric merging primitive in Evd. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Tentative performance fix for Evd.merge_uctx. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | 2014-08-08 |
| * | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
| * | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
| * | Small code simplification. | Pierre-Marie Pédrot | 2014-08-05 |
| * | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | 2014-08-05 |
| * | - Fix handling of opaque polymorphic definitions which were turned transparent. | Matthieu Sozeau | 2014-08-03 |
| * | Move to a representation of universe polymorphic constants using indices for ... | Matthieu Sozeau | 2014-08-03 |
| * | - Fix has_undefined_evars not using its or_sorts argument anymore. | Matthieu Sozeau | 2014-08-03 |
| * | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin | 2014-08-01 |
| * | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
Matthieu Sozeau
Matthieu Sozeau
Arnaud Spiwack
Pierre-Marie Pédrot
Hugo Herbelin
Pierre Boutillier
Jason Gross