aboutsummaryrefslogtreecommitdiff
path: root/printing/ppvernac.ml
AgeCommit message (Collapse)Author
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
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
No other changes (long only because of a change of indentation).
2016-06-16Fixing extra space in printing bullets.Hugo Herbelin
2016-06-16Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
Fixing : in Declare Module.
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
with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance.
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
This reverts commit 9e9620b99f68622ebaf44c43e9945580f6cc6d98.
2016-04-27Revert "Printing notations as parsed."Hugo Herbelin
This reverts commit 92cbd4ed5f9679e46da16e83a2f920449c699a4e.
2016-04-27Revert "Fixing printing of Arguments."Hugo Herbelin
This reverts commit c90d538c8763cb90fab6071cf00236f00b3c33a2.
2016-04-27Revert "Fixing printing of Polymorphic/Monomorphic."Hugo Herbelin
This reverts commit 094ed756fcef1ac5118dc5134a7369252efec933.
2016-04-27Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."Hugo Herbelin
This reverts commit d91a1aa62edad53b41fbb7cb6f6a841f03ebcde4.
2016-04-27Revert "Fixing printing of Instance."Hugo Herbelin
This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
2016-04-27Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."Hugo Herbelin
This reverts commit e11620ce155529c0e577304427f9b05d38e73caf.
2016-04-27Revert "Fixing extra space in printing bullets."Hugo Herbelin
This reverts commit 91ce24b97ee5a8ee67ac11153ab10577c11bc9fc.
2016-04-27Revert "Removing unused generalization of pr_vernac over pr_constr and ↵Hugo Herbelin
pr_lconstr." This reverts commit ee882d4cf6e7d84dc4589535042bbefdec56a288.
2016-04-27Revert "Simplification in ppvernac.ml."Hugo Herbelin
This reverts commit d82c87e40a85be184ede1f9a2fde04dd8f48bb74.
2016-04-27Revert "Isolating and exporting a function for printing body of a recursive ↵Hugo Herbelin
definition." This reverts commit 5598db7882f111b1fe3aa22936679e06b7a2f673.
2016-04-27Revert "Taking into account the original grammar rule to print generic"Hugo Herbelin
This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90.
2016-04-27Revert "Fixing extra space in front of terminal in printing vernac."Hugo Herbelin
This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
2016-04-27Fixing extra space in front of terminal in printing vernac.Hugo Herbelin
fix au revert [||]
2016-04-27Taking into account the original grammar rule to print genericHugo Herbelin
arguments of vernac extensions, so that in list with a separator, the separator is printed.
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
No other changes (long only because of a change of indentation).
2016-04-27Fixing extra space in printing bullets.Hugo Herbelin
2016-04-27Fixing space in printing <+ and <: + fixing missing Inline keyword.Hugo Herbelin
Fixing : in Declare Module.
2016-04-27Fixing printing of Instance.Hugo Herbelin
2016-04-27Fixing extra space in printing abbreviations (SyntaxDefinition).Hugo Herbelin
2016-04-27Fixing printing of Polymorphic/Monomorphic.Hugo Herbelin
2016-04-27Fixing printing of Arguments.Hugo Herbelin
2016-04-27Printing notations as parsed.Hugo Herbelin
2016-04-27So as to beautify to work, do not use notations in Inductive typesHugo Herbelin
with a clause where, nor Notation, nor Fixpoints. Should be certainly improved at least for Inductive types and Fixpoints, depending on whether there is a "where" clause for instance.
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-09Simplifying code for printing VERNAC EXTEND.Hugo Herbelin
2016-04-09Fixing extra space in printing inductive types with no explicit type given.Hugo Herbelin
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Matthieu Sozeau
into JasonGross-trunk-function_scope
2016-03-20Moving the Ltac definition command to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Print Ltac to an EXTEND based command.Pierre-Marie Pédrot
2016-03-20Moving Tactic Notation to an EXTEND based command.Pierre-Marie Pédrot
2016-03-19Moving VernacSolve to an EXTEND-based definition.Pierre-Marie Pédrot
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 22:11:32 +0000