| Age | Commit message (Expand) | Author |
|---|
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Documenting in passing. | Hugo Herbelin |
| 2015-03-04 | Fix bug #3532, providing universe inconsistency information when a | Matthieu Sozeau |
| 2015-02-27 | Add support so that the type of a match in an inductive type with let-in | Hugo Herbelin |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-10-08 | fix make mlidoc | Pierre Boutillier |
| 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-29 | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-13 | Providing a -type-in-type option for collapsing the universe hierarchy. | Hugo Herbelin |
| 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-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 |
| 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-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-03-05 | Remove many superfluous 'open' indicated by ocamlc -w +33 | Pierre Letouzey |
| 2014-02-28 | Dead code elimionation in reductionops | Pierre Boutillier |
| 2014-02-24 | 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 |
| 2013-10-31 | Conv_orable made functional and part of pre_env | gareuselesinge |
| 2013-10-29 | Do not generate useless argument arrays in whd_* functions. | ppedrot |
| 2013-08-25 | Removing association lists in Reductionops. Btw, defining the dual of the | ppedrot |
| 2013-07-19 | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-03-25 | Fix bug #2989: make unification.ml able to deal with canonical structure in a... | pboutill |
| 2013-02-28 | compare_stack_shape before ise_stack2 in evar_conv | pboutill |
| 2013-02-25 | Evarconv: When doing a iota of a fixpoint, use constant name instead of fixpo... | pboutill |
| 2013-01-24 | Reductionops: whd_state_gen can take and answers a cst_stack too | pboutill |
| 2012-12-21 | Awful heuristic to refold mutual fixpoint in reductionops | pboutill |
| 2012-12-19 | Reductionops reduction machine can refold constant | pboutill |
| 2012-12-18 | Modulification of name | ppedrot |
| 2012-08-09 | Unification in Evar_conv uses an abstract machine state | pboutill |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-20 | Reductionops refactoring | pboutill |
| 2012-07-12 | tacred uses stack_reduction_function instead of state_reduction_function | pboutill |
| 2012-06-15 | Reductionops abstract machine uses Zcase & Zfix stack node. | pboutill |
| 2012-06-15 | Reductionops : Better abstract machine stack utilities | pboutill |
| 2012-01-31 | Bug #2041: unfold at betaiotaZETA normalize like unfold | pboutill |
| 2011-10-05 | It happens that the type inference algorithm (pretyping) did not check | herbelin |
| 2011-06-19 | Ensured that the transparency state is used when flag betaiota is on for apply. | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
