| Commit message (Expand) | Author | Age |
|---|
| * | Univs: proper printing of global and local universe names (only |  Matthieu Sozeau | 2015-01-17 |
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| * | Option -type-in-type continued (deactivate test for inferred sort of |  Hugo Herbelin | 2014-11-19 |
| * | Evar normalization is now done eagerly. |  Pierre-Marie Pédrot | 2014-11-10 |
| * | Implement a different strategy to expand primitive projections only when | Matthieu Sozeau | 2014-10-15 |
| * | Tentative fix for a badly used Option.get in Reductionops. | Pierre-Marie Pédrot | 2014-10-12 |
| * | 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-02 |
| * | 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-10-01 |
| * | Simplify evarconv thanks to new delta status of projections, | Matthieu Sozeau | 2014-09-30 |
| * | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau | 2014-09-29 |
| * | 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-27 |
| * | Reductionops: (Co)Fixpoints are always refolded during iota |  Pierre Boutillier | 2014-09-18 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
| * | Cleanup code for looking up projection bodies. | Matthieu Sozeau | 2014-09-06 |
| * | Debug RAKAM | Pierre Boutillier | 2014-08-26 |
| * | Grammar: "avoiding to" isn't proper, either |  Jason Gross | 2014-08-25 |
| * | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau | 2014-08-10 |
| * | - 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 |
| * | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau | 2014-07-29 |
| * | Reduce non-toplevel letins in splay_prod_assum (bug found in Ergo). | Matthieu Sozeau | 2014-07-10 |
| * | Removing dead code. | Pierre-Marie Pédrot | 2014-06-17 |
| * | Adapt simpl/cbn unfolding and refolding machinery to projections, so that |  Matthieu Sozeau | 2014-06-13 |
| * | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau | 2014-06-11 |
| * | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
| * | Make kernel reduction code parametric over the handling of universes, | Matthieu Sozeau | 2014-06-06 |
| * | 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-06-04 |
| * | 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 | 2014-05-26 |
| * | Cst_stack before stack (abstraction leak in whd_gen) | Pierre Boutillier | 2014-05-26 |
| * | cbn: args list instead of arg number | Pierre Boutillier | 2014-05-26 |
| * | Reductionops.Stack.map & Reduction.iterate_whd_gen | Pierre | 2014-05-26 |
| * | - Fixes for canonical structure resolution (check that the initial term indee... | Matthieu Sozeau | 2014-05-06 |
| * | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Remove some dead-code (thanks to ocaml warnings) |  Pierre Letouzey | 2014-03-05 |
| * | Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini... | Pierre Boutillier | 2014-02-28 |
| * | Dead code elimionation in reductionops | Pierre Boutillier | 2014-02-28 |
| * | Ensuring that the module Stack is opaque inside Reductionops. | Pierre-Marie Pédrot | 2014-02-24 |
| * | cbn understands Arguments | Pierre Boutillier | 2014-02-24 |
| * | Simpl_behaviour becomes Reductionops.ReductionBehaviour | Pierre Boutillier | 2014-02-24 |
| * | No more translation array <-> list in Reductionops.Stack | Pierre Boutillier | 2014-02-24 |
| * | Reductionops.Stack.strip* are ready to deal with Shift | Pierre Boutillier | 2014-02-24 |
| * | Reductionops.Stack.app_node is secret | Pierre Boutillier | 2014-02-24 |
| * | app_node, stack, state printers | Pierre Boutillier | 2014-02-24 |
Matthieu Sozeau
Maxime Dénès
Hugo Herbelin
Pierre-Marie Pédrot
Pierre Boutillier
Pierre Boutillier
Jason Gross
Matthieu Sozeau
Pierre Letouzey