aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.mli
AgeCommit message (Expand)Author
2020-09-18Adding debugging printers for Intmap.Hugo Herbelin
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-06-04Move the cbn reduction to its own file, and simplify the RAKAM accordingly.Pierre-Marie Pédrot
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-20Adding a printer for GlobEnv in ocamldebug.Hugo Herbelin
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-14Add aucontext debug printerGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-07Add print_pure_econstr signatureThierry Martinez
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-12-22Cleanup top_printers.mliGaëtan Gilbert
2017-12-22Cleanup debug printers a bit, add generated mli.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:03:17 +0000