aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppvernac.ml
Commit message (Expand)AuthorAge
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Revert "So as to beautify to work, do not use notations in Inductive types"Gravatar Hugo Herbelin2016-04-27
* Revert "Printing notations as parsed."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Arguments."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Polymorphic/Monomorphic."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Instance."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing extra space in printing bullets."Gravatar Hugo Herbelin2016-04-27
* Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...Gravatar Hugo Herbelin2016-04-27
* Revert "Simplification in ppvernac.ml."Gravatar Hugo Herbelin2016-04-27
* Revert "Isolating and exporting a function for printing body of a recursive d...Gravatar Hugo Herbelin2016-04-27
* Revert "Taking into account the original grammar rule to print generic"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing extra space in front of terminal in printing vernac."Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in front of terminal in printing vernac.Gravatar Hugo Herbelin2016-04-27
* Taking into account the original grammar rule to print genericGravatar Hugo Herbelin2016-04-27
* Isolating and exporting a function for printing body of a recursive definition.Gravatar Hugo Herbelin2016-04-27
* Simplification in ppvernac.ml.Gravatar Hugo Herbelin2016-04-27
* Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in printing bullets.Gravatar Hugo Herbelin2016-04-27
* Fixing space in printing <+ and <: + fixing missing Inline keyword.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Instance.Gravatar Hugo Herbelin2016-04-27
* Fixing extra space in printing abbreviations (SyntaxDefinition).Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Polymorphic/Monomorphic.Gravatar Hugo Herbelin2016-04-27
* Fixing printing of Arguments.Gravatar Hugo Herbelin2016-04-27
* Printing notations as parsed.Gravatar Hugo Herbelin2016-04-27
* So as to beautify to work, do not use notations in Inductive typesGravatar Hugo Herbelin2016-04-27
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Simplifying code for printing VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
* Fixing extra space in printing inductive types with no explicit type given.Gravatar Hugo Herbelin2016-04-09
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\ \
| * | Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* | | Tying the loop in tactic printing API.Gravatar Pierre-Marie Pédrot2015-12-18
|/ /
* | Adding syntax "Show id" to show goal named id (shelved or not).Gravatar Hugo Herbelin2015-11-02
* | Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* | Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
* | Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 04:04:27 +0000