aboutsummaryrefslogtreecommitdiff
path: root/pretyping/reductionops.ml
AgeCommit message (Expand)Author
2018-02-10Factorize code for comparing maybe-cumulative inductives.Gaëtan Gilbert
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2017-12-30Using a dedicated type for Lib.abstr_info.Pierre-Marie Pédrot
2017-12-14Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Maxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-12Further clean-up in Reductionops, removing unused lift arguments.Maxime Dénès
2017-12-09[api] Remove yet another type alias.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-06Getting rid of the Update constructor in Reductionops.Pierre-Marie Pédrot
2017-12-06Getting rid of the Shift constructor in Reductionops.Pierre-Marie Pédrot
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6117: Fix printing anomaly in convMaxime Dénès
2017-11-08Fixing missing separator in an error message.Hugo Herbelin
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-08Using EConstr equality check in unification.Pierre-Marie Pédrot
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-20Merge branch 'v8.7'Maxime Dénès
2017-07-11Deprecate options that were introduced for compatibility with 8.5.Théo Zimmermann
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-06-16Use inductive subtyping for conv/cumulAmin Timany
2017-06-13Merge PR#714: Print feature Proof-of-Concept (episode 2)Maxime Dénès
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-04Added support for a side effect on constants in reduction functions.Thomas Sibut-Pinote
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#670: Postponing of universe constraints unification in term equality.Maxime Dénès
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-23Postponing of universe constraints unification in term equality.Pierre-Marie Pédrot
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-13Reinstate fixpoint refolding in [cbn], deactivated by mistake.Matthieu Sozeau
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Cc API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:46:55 +0000