aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
Commit message (Expand)AuthorAge
* Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* no-refold patchGravatar Paul Steckler2016-09-09
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* Make semantics of whd_zeta consistent with other whd_* functions.Gravatar Maxime Dénès2016-07-01
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-02
|/ /
* / CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
|/
* Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
* Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Documenting in passing.Gravatar Hugo Herbelin2015-08-02
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
* Add support so that the type of a match in an inductive type with let-inGravatar Hugo Herbelin2015-02-27
* Update headers.Gravatar Maxime Dénès2015-01-12
* fix make mlidocGravatar Pierre Boutillier2014-10-08
* Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.Gravatar Matthieu Sozeau2014-10-02
* Fix cbn behavior wrt simpl no matchGravatar Pierre Boutillier2014-10-01
* Fix the refolding by cbn of mutal constants defined in not included modulesGravatar Pierre Boutillier2014-10-01
* In evarconv and unification, expand folded primitive projections toGravatar Matthieu Sozeau2014-09-29
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* cbn understand ! Arguments directiveGravatar Pierre Boutillier2014-06-04
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
* Reduction.Stack.Fix/Case stores Cst_stack.tGravatar Pierre Boutillier2014-05-26
* Cst_stack before stack (abstraction leak in whd_gen)Gravatar Pierre Boutillier2014-05-26
* cbn: args list instead of arg numberGravatar Pierre Boutillier2014-05-26
* Reductionops.Stack.map & Reduction.iterate_whd_genGravatar Pierre2014-05-26
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Dead code elimionation in reductionopsGravatar Pierre Boutillier2014-02-28
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.strip* are ready to deal with ShiftGravatar Pierre Boutillier2014-02-24
* Reductionops.Stack.app_node is secretGravatar Pierre Boutillier2014-02-24
* app_node, stack, state printersGravatar Pierre Boutillier2014-02-24
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29