aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/pptactic.ml
AgeCommit message (Expand)Author
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
2017-11-24Extending further PR#6047 (system to register printers for Ltac values).Hugo Herbelin
2017-11-24Printing again "intros **" as "intros" by default.Hugo Herbelin
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
2017-11-15Fixing printing of tactics encapsulated as tacarg with Tacexp.Hugo Herbelin
2017-11-15Using "l" printer for glob_constr, like for constr.Hugo Herbelin
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04Adding support for syntax "let _ := e in e'" in Ltac.Hugo Herbelin
2017-11-02Binding ltac printing functions to the system of generic printing.Hugo Herbelin
2017-11-02Setting a system to register printers for Ltac values.Hugo Herbelin
2017-11-02Using a specific function to register vernac printers.Hugo Herbelin
2017-11-02Exporting a few more printing functions.Hugo Herbelin
2017-10-03Moving the Ltac-specific part of the nametab to the Ltac plugin.Pierre-Marie Pédrot
2017-10-03Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Maxime Dénès
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-09-26Properly display the "only" prefix for selectors (bug #5760).Guillaume Melquiond
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-29A new step of restructuration of notations.Hugo Herbelin
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-06Merge PR#716: Don't double up on periods in anomaliesMaxime Dénès
2017-06-05Merge PR#722: [printing] Remove duplicated printing function.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-06-01[printing] Remove duplicated printing function.Emilio Jesus Gallego Arias
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-30Adding "epose", "eset", "eremember" which allow to set terms withHugo Herbelin
2017-05-30Adding "eassert", "eenough", "epose proof", which allow to stateHugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-16Adding support for using grammar entries returning no value in EXTEND.Hugo Herbelin
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] [ast] Switch Constrexpr AST to an extensible node type.Emilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in tactics.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-03-24Merge branch 'trunk' into pr379Maxime Dénès
2017-03-21[pp] Move terminal-specific tagging to the toplevel.Emilio Jesus Gallego Arias
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:48:37 +0000