aboutsummaryrefslogtreecommitdiff
path: root/printing
AgeCommit message (Expand)Author
2018-12-17Merge PR #9153: [api] Move reduction modules to `tactics`Pierre-Marie Pédrot
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-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
2018-12-10Fix Invalid_argument in List.iter2Jim Fehrle
2018-12-10For diffs, return exactly the characters that make up STRING and FIELD tokensJim Fehrle
2018-12-10Fix #9091: don't show deleted compacted hypotheses twice in diffJim Fehrle
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-21Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlibEnrico Tassi
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
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-19Move transparent_state to its own module.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-05Merge PR #8871: [library] Move Nametab/Lib specific-names to NametabHugo Herbelin
2018-11-02Remove is_universe_polymorphism from printingGaëtan Gilbert
2018-10-31[nametab] Move `object_prefix` to `Nametab`.Emilio Jesus Gallego Arias
2018-10-31[nametab] Move global_dir_reference to NametabEmilio Jesus Gallego Arias
2018-10-31Merge PR #8825: [libobject] Move object_name next to object definition.Pierre-Marie Pédrot
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-26[libobject] Move object_name next to object definition.Emilio Jesus Gallego Arias
2018-10-26Merge PR #8687: Mini reorganization type of global constr of globalPierre-Marie Pédrot
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
2018-10-11Merge PR #8680: Check that lambda/prod ast's have proper binders during inter...Emilio Jesus Gallego Arias
2018-10-11Check that lambda/prod ast's have proper binders during interning/printing.Lasse Blaauwbroek
2018-10-10Miscellaneous refinements/cleaning of module printing.Hugo Herbelin
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-29Replacing Refine.pr_constr by Termops.Internal.print_constr.Hugo Herbelin
2018-09-27Merge PR #6524: [print] Restrict use of "debug" Termops printer.Pierre-Marie Pédrot
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-23Merge PR #8247: Show diffs on multiple changed goals; match old and new goal ...Emilio Jesus Gallego Arias
2018-09-21Store universe binder names as a mere list of names.Pierre-Marie Pédrot
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 23:05:47 +0000