aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Expand)Author
2017-06-16Add printing of cumulativity in inductive typesAmin Timany
2017-06-16Fix bugs and add an option for cumulativityAmin Timany
2017-06-12[proof] Move bullets to their own module.Emilio Jesus Gallego Arias
2017-06-12Remove Show Thesis command which was never implemented.Théo Zimmermann
2017-06-12Remove non-working Show Tree and Show Node commands.Théo Zimmermann
2017-06-12Remove Show Implicit Arguments command.Théo Zimmermann
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Maxime Dénès
2017-04-27Remove some unused values and typesGaetan 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-24[location] Use Loc.located for constr_expr.Emilio Jesus Gallego Arias
2017-04-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-21Remove VernacErrorGaetan Gilbert
2017-04-20refactoring "Ppvernac.pr_extend"Matej Kosik
2017-04-09Removing internal support for accepting "{struct x}" and co in "Theorem with".Hugo Herbelin
2017-03-24[stm] Remove some obsolete vernacs/classification.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-12-02Fixing printing of "Set Warnings Append".Hugo Herbelin
2016-12-02Fixing space in printing "Context".Hugo Herbelin
2016-12-02Fixing space in printing several list of implicit arguments.Hugo Herbelin
2016-12-02Fixing printing of "only parsing" in abbreviations.Hugo Herbelin
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-18Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"Maxime Dénès
2016-11-17[stm] Remove STM-related vernacularsEmilio Jesus Gallego Arias
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Fixing a few confusions on the name of the beautify flag.Hugo Herbelin
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-08Unplugging Pptactic from Ppvernac.Pierre-Marie Pédrot
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:52:02 +0000