aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.mli
AgeCommit message (Expand)Author
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-24Remove the unused printer_pr mechanism.Jim Fehrle
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-08Merge PR #6816: Adding mention of shelved/given-up status in Show ExistentialsMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22Adding mention of shelved/given-up status in "Show Existentials".Hugo Herbelin
2018-02-11Print inductive cumulativity info in About.Gaëtan Gilbert
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-11-29[proof] [api] Rename proof types in preparation for functionalization.Emilio Jesus Gallego Arias
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6103: Hack to restore printing of glob_constr in debugger.Maxime Dénès
2017-11-07Hack to restore printing of glob_constr in debugger.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-11-04Finish removing Show Goal uidGaëtan Gilbert
2017-11-02Exporting the level-parametric printer of constr and its variants.Hugo Herbelin
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Add printing of cumulativity in inductive typesAmin Timany
2017-06-16Using UInfoInd for universes in inductive typesAmin Timany
2017-06-01[emacs] [toplevel] Make emacs flag local to the toplevel.Emilio Jesus Gallego Arias
2017-05-17Merge PR#457: Adding an even more compact goal hyps mode.Maxime Dénès
2017-05-04Adding an option "Printing Unfocused".Pierre Courtieu
2017-05-03Adding an even more compact mode for goal display.Pierre Courtieu
2017-02-14Removing compatibility layers related to printing.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2016-08-26CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl"Matej Kosik
2016-08-26CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Matej Kosik
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-11-02Adding syntax "Show id" to show goal named id (shelved or not).Hugo Herbelin
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Printing of @{} instances for polymorphic references in Print and About.Matthieu Sozeau
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-03-31Generalisation of the "end command" argument of the goal printer.Arnaud Spiwack
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-04Improving error message when one instance-hole is not found.Hugo Herbelin
2014-11-20Moving mutual inductive printing from Printer to Printmod.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:41:56 +0000