| Commit message (Expand) | Author | Age |
* | 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 |
* | Stack operations of Reductionops in Reductionops.Stack | Pierre Boutillier | 2014-02-24 |
* | Removing partial applications in Reductionops. | ppedrot | 2013-11-08 |
* | Preventing useless allocations in Reductionops.instance. | ppedrot | 2013-11-05 |
* | 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 |
* | [Reductionops.append_stack_app]: do not allocate a useless array. | ppedrot | 2013-10-29 |
* | Various optimizations in Constr, such as term sharing and allocation | ppedrot | 2013-10-22 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | 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 |
* | Minor code cleaning in CArray / CList. | ppedrot | 2013-03-23 |
* | Typo in an error message | letouzey | 2013-03-14 |
* | Restrict (try...with...) to avoid catching critical exn (part 7) | letouzey | 2013-03-13 |
* | More monomorphization. | ppedrot | 2013-03-05 |
* | 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 |
* | Dir_path --> DirPath | letouzey | 2013-02-19 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Added backtrace information to anomalies | ppedrot | 2013-01-28 |
* | Reductionops: whd_state_gen can take and answers a cst_stack too | pboutill | 2013-01-24 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |