aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
Commit message (Expand)AuthorAge
* [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
| * | Postponing of universe constraints unification in term equality.Gravatar Pierre-Marie Pédrot2017-05-23
|/ /
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * Reinstate fixpoint refolding in [cbn], deactivated by mistake.Gravatar Matthieu Sozeau2017-04-13
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing some return type compatibility layers in Termops.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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 07:28:35 +0000