| Commit message (Expand) | Author | Age |
|---|
| * | no-refold patch |  Paul Steckler | 2016-09-09 |
| * | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module) |  Pierre Letouzey | 2016-07-03 |
| * | Make semantics of whd_zeta consistent with other whd_* functions. |  Maxime Dénès | 2016-07-01 |
| * | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès | 2016-07-01 |
| * | Using monotonic types for conversion functions. |  Pierre-Marie Pédrot | 2016-02-15 |
| * | Merge branch 'v8.5' | Pierre-Marie Pédrot | 2016-01-21 |
| |\ |
|
| | * | Update copyright headers. | Maxime Dénès | 2016-01-20 |
| * | | merge |  Matej Kosik | 2016-01-11 |
| |\ \ |
|
| | * | | CLEANUP: kernel/context.ml{,i} | Matej Kosik | 2016-01-11 |
| * | | | Remove duplicate declarations. |  Guillaume Melquiond | 2016-01-02 |
| |/ / |
|
| * / | CLEANUP: in the Reductionops module | Matej Kosik | 2015-12-17 |
| |/ |
|
| * | 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-10-15 |
| * | Reverting 16 last commits, committed mistakenly using the wrong push command. |  Hugo Herbelin | 2015-08-02 |
| * | Documenting in passing. | Hugo Herbelin | 2015-08-02 |
| * | Fix bug #3532, providing universe inconsistency information when a |  Matthieu Sozeau | 2015-03-04 |
| * | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin | 2015-02-27 |
| * | Update headers. | Maxime Dénès | 2015-01-12 |
| * | fix make mlidoc |  Pierre Boutillier | 2014-10-08 |
| * | 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 |
| * | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau | 2014-09-29 |
| * | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau | 2014-09-27 |
| * | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin | 2014-09-13 |
| * | 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 |
| * | 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 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey | 2014-03-05 |
| * | Dead code elimionation in reductionops | Pierre Boutillier | 2014-02-28 |
| * | Simpl_behaviour becomes Reductionops.ReductionBehaviour | 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 |
| * | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier | 2014-02-24 |
| * | Conv_orable made functional and part of pre_env |  gareuselesinge | 2013-10-31 |
| * | Do not generate useless argument arrays in whd_* functions. |  ppedrot | 2013-10-29 |
| * | Removing association lists in Reductionops. Btw, defining the dual of the | ppedrot | 2013-08-25 |
| * | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... |  msozeau | 2013-07-19 |
| * | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
| * | Fix bug #2989: make unification.ml able to deal with canonical structure in a... |  pboutill | 2013-03-25 |
| * | compare_stack_shape before ise_stack2 in evar_conv | pboutill | 2013-02-28 |
| * | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... | pboutill | 2013-02-25 |
Paul Steckler
Pierre Letouzey
Maxime Dénès
Pierre-Marie Pédrot
Matej Kosik
Guillaume Melquiond
Hugo Herbelin
Matthieu Sozeau
Pierre Boutillier
Pierre Boutillier
Matthieu Sozeau
gareuselesinge
ppedrot
msozeau
pboutill