aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
Commit message (Expand)AuthorAge
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
* Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6769: Split closure cache and remove whd_bothGravatar Maxime Dénès2018-03-09
|\ \
| | * Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
| | * Statically enforce that ULub is only between levels.Gravatar Gaëtan Gilbert2018-03-09
| | * Option for messing with inference of irrelevant constraintsGravatar Gaëtan Gilbert2018-03-09
| | * Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | * Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| |/ |/|
* | [compat] Remove "Refolding Reduction" option.Gravatar Emilio Jesus Gallego Arias2018-03-08
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \
* | | reductionops: remove dead code "bind_assum"Gravatar Enrico Tassi2018-03-04
| | * Pass the constant cache as a separate argument in kernel reduction.Gravatar Pierre-Marie Pédrot2018-03-04
| |/ |/|
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
* Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Using a dedicated type for Lib.abstr_info.Gravatar Pierre-Marie Pédrot2017-12-30
* Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Gravatar Maxime Dénès2017-12-14
|\
* \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \
| | * Further clean-up in Reductionops, removing unused lift arguments.Gravatar Maxime Dénès2017-12-12
| |/ |/|
* | [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
|/
* Getting rid of the Update constructor in Reductionops.Gravatar Pierre-Marie Pédrot2017-12-06
* Getting rid of the Shift constructor in Reductionops.Gravatar Pierre-Marie Pédrot2017-12-06
* Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
* Merge PR #6098: [api] Move structures deprecated in the API to the core.Gravatar Maxime Dénès2017-11-13
|\
* \ Merge PR #6117: Fix printing anomaly in convGravatar Maxime Dénès2017-11-13
|\ \
| * | Fixing missing separator in an error message.Gravatar Hugo Herbelin2017-11-08
| | * [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
|/
* Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\
| * Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
* | Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
* Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* | | 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
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ |/|
* | Merge PR#670: Postponing of universe constraints unification in term equality.Gravatar Maxime Dénès2017-06-01
|\ \
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:41:35 +0000