aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Expand)Author
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-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-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-12Fixing a few confusions on the name of the beautify flag.Hugo Herbelin
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-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
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
2016-06-16Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-06-16Simplification in ppvernac.ml.Hugo Herbelin
2016-06-16Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
2016-06-16Fixing extra space in printing bullets.Hugo Herbelin
2016-06-16Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
2016-06-16Fixing printing of Instance.Hugo Herbelin
2016-06-16Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-06-16Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-06-16Fixing printing of Arguments.Hugo Herbelin
2016-06-16Printing notations as parsed.Hugo Herbelin
2016-06-16So as to beautify to work, do not use notations in Inductive typesHugo Herbelin
2016-06-07Adding an only printing flag to notations.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-04-27Revert "So as to beautify to work, do not use notations in Inductive types"Hugo Herbelin
2016-04-27Revert "Printing notations as parsed."Hugo Herbelin
2016-04-27Revert "Fixing printing of Arguments."Hugo Herbelin
2016-04-27Revert "Fixing printing of Polymorphic/Monomorphic."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Hugo Herbelin
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
2016-04-27Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Hugo Herbelin
2016-04-27Revert "Fixing extra space in printing bullets."Hugo Herbelin
2016-04-27Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...Hugo Herbelin
2016-04-27Revert "Simplification in ppvernac.ml."Hugo Herbelin
2016-04-27Revert "Isolating and exporting a function for printing body of a recursive d...Hugo Herbelin
2016-04-27Revert "Taking into account the original grammar rule to print generic"Hugo Herbelin
2016-04-27Revert "Fixing extra space in front of terminal in printing vernac."Hugo Herbelin
2016-04-27Fixing extra space in front of terminal in printing vernac.Hugo Herbelin
2016-04-27Taking into account the original grammar rule to print genericHugo Herbelin
2016-04-27Isolating and exporting a function for printing body of a recursive definition.Hugo Herbelin
2016-04-27Simplification in ppvernac.ml.Hugo Herbelin
2016-04-27Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Hugo Herbelin
2016-04-27Fixing extra space in printing bullets.Hugo Herbelin
2016-04-27Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin