| Age | Commit message (Expand) | Author |
|---|
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-11-22 | Fixing kernel bug in typing match with let-ins in the arity. | Hugo Herbelin |
| 2015-11-09 | Pushing the backtrace in conversion anomalies. | Pierre-Marie Pédrot |
| 2015-10-28 | Conversion of polymorphic inductive types was incomplete in VM and native. | Maxime Dénès |
| 2015-10-15 | Avoid dependency of the pretyper on C code. | Maxime Dénès |
| 2015-10-15 | Fix #4346 2/2: VM casts were not inferring universe constraints. | Maxime Dénès |
| 2015-10-15 | Fix #4346 1/2: native casts were not inferring universe constraints. | Maxime Dénès |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Hopefully clearer printing of stack when debugging evarconv unification. | Hugo Herbelin |
| 2015-06-28 | Fix incompleteness of conversion used by evarconv | Matthieu Sozeau |
| 2015-03-04 | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau |
| 2015-03-03 | Fix bug #4103: forgot to allow unfolding projections of cofixpoints like | Matthieu Sozeau |
| 2015-02-27 | simpl: honor Global for "simpl: never" (Close: 3206) | Enrico Tassi |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin |
| 2015-02-21 | Fixing bug #3071. | Pierre-Marie Pédrot |
| 2015-02-15 | Fix 'don't expose cases' in cbn | Pierre Boutillier |
| 2015-01-17 | Univs: proper printing of global and local universe names (only | Matthieu Sozeau |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-11-19 | Option -type-in-type continued (deactivate test for inferred sort of | Hugo Herbelin |
| 2014-11-10 | Evar normalization is now done eagerly. | Pierre-Marie Pédrot |
| 2014-10-15 | Implement a different strategy to expand primitive projections only when | Matthieu Sozeau |
| 2014-10-12 | Tentative fix for a badly used Option.get in Reductionops. | Pierre-Marie Pédrot |
| 2014-10-02 | Work around issues with FO unification trying to unify terms of | Matthieu Sozeau |
| 2014-10-02 | Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv. | Matthieu Sozeau |
| 2014-10-01 | Fix cbn behavior wrt simpl no match | Pierre Boutillier |
| 2014-10-01 | Fix the refolding by cbn of mutal constants defined in not included modules | Pierre Boutillier |
| 2014-09-30 | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau |
| 2014-09-29 | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau |
| 2014-09-27 | Fix bug #3664 by refolding projections that don't reduce in cbn. | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-18 | Reductionops: (Co)Fixpoints are always refolded during iota | Pierre Boutillier |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 2014-09-06 | Cleanup code for looking up projection bodies. | Matthieu Sozeau |
| 2014-08-26 | Debug RAKAM | Pierre Boutillier |
| 2014-08-25 | Grammar: "avoiding to" isn't proper, either | Jason Gross |
| 2014-08-10 | Fix bug introduced by earlier commit on first-order unification of primitive | 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-07-29 | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau |
| 2014-07-10 | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-13 | Adapt simpl/cbn unfolding and refolding machinery to projections, so that | Matthieu Sozeau |
| 2014-06-11 | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-06 | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-06-04 | - Keep all <= constraints during refinement, otherwise we might miss collapse... | Matthieu Sozeau |
| 2014-06-04 | cbn understand ! Arguments directive | Pierre Boutillier |
| 2014-05-26 | Cbn reduces Pos.compare p~1 q~1 to Pos.compare p q | Pierre Boutillier |
| 2014-05-26 | Reduction.Stack.Fix/Case stores Cst_stack.t | Pierre Boutillier |
