aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/changes.md
AgeCommit message (Expand)Author
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is de...Hugo Herbelin
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-09-28Document the ocamlformat changes.Pierre-Marie Pédrot
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-05-18Update to 8.13.Théo Zimmermann
2020-04-15[dev] [doc] Changes.Emilio Jesus Gallego Arias
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-19[ocamformat] Update to 0.13.0Emilio Jesus Gallego Arias
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-01-15[ocaml] Remove Custom Backtrace module in favor of OCaml'sEmilio Jesus Gallego Arias
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-10-16[engine] Remove UnivGen.global_of_constrVincent Laporte
2019-06-24[proof] dev/doc/changes for the last refactoringsEmilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-05-21Fixing typos - Part 1JPR
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-29Revert #8187Vincent Laporte
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
2019-04-16[doc] Changes for coq/coq#9165Emilio Jesus Gallego Arias
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Documentation for SPropGaëtan Gilbert
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-04Addressing issues with PR#873: performance and use of abbreviation for printing.Hugo Herbelin
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-02Add dev/changes about attribute syntax in mlgGaëtan Gilbert
2018-10-15Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-06Merge PR #8555: Remove section paths from kernel namesPierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-05Adapt changes to backported commits.Guillaume Melquiond
2018-10-05Improve markdown in changes.Guillaume Melquiond
2018-10-02Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.Pierre-Marie Pédrot
2018-10-02Document the coqpp implementation of VERNAC EXTEND.Pierre-Marie Pédrot
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-02Documenting the syntax changes.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:07:21 +0000