| Age | Commit message (Expand) | Author |
|---|
| 2014-09-10 | Fix generation of inductive elimination principle for primitive records. | Matthieu Sozeau |
| 2014-09-06 | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau |
| 2014-09-05 | Fix checker treatment of inductives using subst_instances instead of subst_un... | Matthieu Sozeau |
| 2014-09-05 | Rename eta_expand_ind_stacks, fix the one from the checker and adapt | Matthieu Sozeau |
| 2014-09-05 | Fix primitive projections declarations for inductive records. | 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-01 | Coqide prints succesive hyps of the same type on 1 line | Pierre Boutillier |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-29 | Add test-suite file. Compute the name for the record binder in the | Matthieu Sozeau |
| 2014-08-28 | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-18 | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger... | Matthieu Sozeau |
| 2014-08-14 | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau |
| 2014-08-13 | Small optimization in Cooking: do not construct identity substitutions. | Pierre-Marie Pédrot |
| 2014-08-09 | Adding a primitive to merge ContextSets which is more efficient when one | Pierre-Marie Pédrot |
| 2014-08-09 | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot |
| 2014-08-06 | Relax a bit the guard condition. | Maxime Dénès |
| 2014-08-05 | make a few lines fit the screen | Enrico Tassi |
| 2014-08-04 | One more optimization for guard checking of cofixpoints. | Maxime Dénès |
| 2014-08-04 | More optimization in guard checking. | Maxime Dénès |
| 2014-08-04 | Fix an exponential behavior in guard checker for cofixpoints. | Maxime Dénès |
| 2014-08-04 | Fixing semantics of Univ.Level.equal. | Pierre-Marie Pédrot |
| 2014-08-03 | Fix infer conv using the wrong universe conversion flexibility information | Matthieu Sozeau |
| 2014-08-03 | - 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-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-07-31 | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot |
| 2014-07-31 | Optimize check of new subterm relation on match. | Maxime Dénès |
| 2014-07-31 | Fix dynamic computation of recargs for mutual inductives. | Maxime Dénès |
| 2014-07-30 | Avoid hconsing instances during appends and conversions from/to arrays. | Matthieu Sozeau |
| 2014-07-29 | Fix eta-conversion code which was failing in nested cases. Fixes bug #3429. | Matthieu Sozeau |
| 2014-07-25 | - Do module substitution inside mind_record. | Matthieu Sozeau |
| 2014-07-22 | Minor cleaning. | Maxime Dénès |
| 2014-07-22 | Revert "Extend subterm relation to pattern matching in return predicates." | Maxime Dénès |
| 2014-07-22 | Revert "Propagate size info through pattern matching in predicates, for the" | Maxime Dénès |
| 2014-07-22 | Propagate size info through pattern matching in predicates, for the | Maxime Dénès |
| 2014-07-22 | Extend subterm relation to pattern matching in return predicates. | Maxime Dénès |
| 2014-07-22 | Fix check_inductive_codomain. | Maxime Dénès |
| 2014-07-22 | Refine check_is_subterm. | Maxime Dénès |
| 2014-07-22 | Refined guard condition of cofixpoints, to anticipate potential futur | Maxime Dénès |
| 2014-07-22 | First attempt at a fix for guard condition on cofixpoints. | Maxime Dénès |
| 2014-07-22 | Typo in comment. | Maxime Dénès |
| 2014-07-22 | Made intersection on regular trees less intensional. | Maxime Dénès |
| 2014-07-22 | Refining match subterm and commutative cut rules. The parameters that are | Maxime Dénès |
| 2014-07-22 | Tentative fix for the commutative cut subterm rule. | Maxime Dénès |
| 2014-07-22 | Tentative patch for incompatibility between subterm relation and dependent | Maxime Dénès |
| 2014-07-21 | Universe level maps use HMaps. | Pierre-Marie Pédrot |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau |
| 2014-07-21 | Cleanup code for constant equality in kernel conversion. | Matthieu Sozeau |
