| Commit message (Expand) | Author | Age |
|---|
| * | Revert "Move eta-expansion after delta reduction in kernel reduction. This ma... |  Matthieu Sozeau | 2014-10-14 |
| * | selective join/export of the safe_environment |  Enrico Tassi | 2014-10-13 |
| * | STM: simplify how the term part of a side effect is retrieved | Enrico Tassi | 2014-10-13 |
| * | library/opaqueTables: enable their use in interactive mode | Enrico Tassi | 2014-10-13 |
| * | Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name |  Matthieu Sozeau | 2014-10-11 |
| * | Fix segfault in native compiler on int31 division. |  Maxime Dénès | 2014-10-10 |
| * | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau | 2014-10-02 |
| * | Move eta-expansion after delta reduction in kernel reduction. This makes | Matthieu Sozeau | 2014-10-02 |
| * | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau | 2014-09-30 |
| * | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
| * | Make the retroknowledge marshalable. |  Arnaud Spiwack | 2014-09-24 |
| * | Clean a bit of univ.ml, add credits. | Matthieu Sozeau | 2014-09-18 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. |  Hugo Herbelin | 2014-09-13 |
| * | Fix generation of inductive elimination principle for primitive records. | Matthieu Sozeau | 2014-09-10 |
| * | Fix checker to handle projections with eta and universe polymorphism correctly. | Matthieu Sozeau | 2014-09-06 |
| * | 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-05 |
| * | 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 |
| * | Coqide prints succesive hyps of the same type on 1 line |  Pierre Boutillier | 2014-09-01 |
| * | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
| * | Add test-suite file. Compute the name for the record binder in the | Matthieu Sozeau | 2014-08-29 |
| * | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
| * | "allows to", like "allowing to", is improper |  Jason Gross | 2014-08-25 |
| * | Fix pretty-printing of the graph in Print Sorted Universes. Type.0 was larger... | Matthieu Sozeau | 2014-08-18 |
| * | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | 2014-08-14 |
| * | Small optimization in Cooking: do not construct identity substitutions. |  Pierre-Marie Pédrot | 2014-08-13 |
| * | 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-09 |
| * | Relax a bit the guard condition. | Maxime Dénès | 2014-08-06 |
| * | make a few lines fit the screen | Enrico Tassi | 2014-08-05 |
| * | 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-04 |
| * | 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-03 |
| * | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
| * | 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-31 |
| * | Avoid hconsing instances during appends and conversions from/to arrays. | Matthieu Sozeau | 2014-07-30 |
| * | Fix eta-conversion code which was failing in nested cases. Fixes bug #3429. | Matthieu Sozeau | 2014-07-29 |
| * | - Do module substitution inside mind_record. | Matthieu Sozeau | 2014-07-25 |
| * | 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 |
Matthieu Sozeau
Enrico Tassi
Matthieu Sozeau
Maxime Dénès
Arnaud Spiwack
Hugo Herbelin
Pierre Boutillier
Jason Gross
Pierre-Marie Pédrot