aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
AgeCommit message (Expand)Author
2020-09-01Unify the shelvesMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-07-15Do not print global refs as terms when asked to be printed as themselves.Hugo Herbelin
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-02-20Merge PR #11143: In Print/Check/Show, adopt the view that the attached type i...Emilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-08When printing term together with its type, use info that term is in context.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
2019-08-16Improve [Print Assumptions] for type-in-type and assumed positive.SimonBoulier
2019-08-16Add [Print Typing Flags] command.SimonBoulier
2019-07-11[proof] Minor cleanup in proof.mlEmilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-12Merge PR #9101: Fix 8922 againHugo Herbelin
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-27Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...Emilio Jesus Gallego Arias
2018-11-23Fix printing of private universes.Gaëtan Gilbert
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
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-16Print universe names in subtyping error instead of Var(x).Gaëtan Gilbert
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:57:35 +0000