aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.mli
Commit message (Expand)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\
* | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| * Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
|/
* Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 01:52:11 +0000