index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
printing
Commit message (
Expand
)
Author
Age
...
*
|
|
Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"
Hugo Herbelin
2016-04-27
*
|
|
Revert "Printing notations as parsed."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing printing of Arguments."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing printing of Polymorphic/Monomorphic."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing extra space in printing abbreviations (SyntaxDefinition)."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing printing of Instance."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing space in printing <+ and <: + fixing missing Inline keyword."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing extra space in printing bullets."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Removing unused generalization of pr_vernac over pr_constr and pr_lco...
Hugo Herbelin
2016-04-27
*
|
|
Revert "Simplification in ppvernac.ml."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Isolating and exporting a function for printing body of a recursive d...
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing printing of Register retroknowledge."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Passing around the precedence to the generic printer so as to solve"
Hugo Herbelin
2016-04-27
*
|
|
Revert "Temporary hack to restore missing printing of "constr:" in right-hand"
Hugo Herbelin
2016-04-27
*
|
|
Revert "Taking into account the original grammar rule to print generic"
Hugo Herbelin
2016-04-27
*
|
|
Revert "Fixing extra space in front of terminal in printing vernac."
Hugo Herbelin
2016-04-27
*
|
|
Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...
Hugo Herbelin
2016-04-27
*
|
|
Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"
Hugo Herbelin
2016-04-27
*
|
|
Fixing extra space in front of terminal in printing vernac.
Hugo Herbelin
2016-04-27
*
|
|
Taking into account the original grammar rule to print generic
Hugo Herbelin
2016-04-27
*
|
|
Temporary hack to restore missing printing of "constr:" in right-hand
Hugo Herbelin
2016-04-27
*
|
|
Passing around the precedence to the generic printer so as to solve
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of Register retroknowledge.
Hugo Herbelin
2016-04-27
*
|
|
Isolating and exporting a function for printing body of a recursive definition.
Hugo Herbelin
2016-04-27
*
|
|
Simplification in ppvernac.ml.
Hugo Herbelin
2016-04-27
*
|
|
Removing unused generalization of pr_vernac over pr_constr and pr_lconstr.
Hugo Herbelin
2016-04-27
*
|
|
Fixing extra space in printing bullets.
Hugo Herbelin
2016-04-27
*
|
|
Fixing space in printing <+ and <: + fixing missing Inline keyword.
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of Instance.
Hugo Herbelin
2016-04-27
*
|
|
Fixing extra space in printing abbreviations (SyntaxDefinition).
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of Polymorphic/Monomorphic.
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of Arguments.
Hugo Herbelin
2016-04-27
*
|
|
Printing notations as parsed.
Hugo Herbelin
2016-04-27
*
|
|
Revert "Protect printing of intro-patterns from collision when "[|" or
Hugo Herbelin
2016-04-27
*
|
|
Protect printing of ltac's "context [...]" from possible collision
Hugo Herbelin
2016-04-27
*
|
|
Protect printing of intro-patterns from collision when "[|" or "|]"
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of keeping hyp on the fly.
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of inversion as.
Hugo Herbelin
2016-04-27
*
|
|
Fixing extra space in printing destruct/induction as.
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of induction/destruct as.
Hugo Herbelin
2016-04-27
*
|
|
Fixing printing of pat%constr.
Hugo Herbelin
2016-04-27
*
|
|
Honor parsing and printing levels for tactic entry in TACTIC EXTEND and
Hugo Herbelin
2016-04-27
*
|
|
Temporary deactivate re-interpretation of terms in beautify.
Hugo Herbelin
2016-04-27
*
|
|
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
|
|
So as to beautify to work, do not use notations in Inductive types
Hugo Herbelin
2016-04-27
*
|
|
A heuristic to add parentheses in the presence of rules such as
Hugo Herbelin
2016-04-27
*
|
|
Attempt to slightly improve abusive "Collision between bound
Hugo Herbelin
2016-04-27
*
|
|
Removing dead code related to printing of ML tactics in Pptactic.
Pierre-Marie Pédrot
2016-04-25
|
*
|
Revert "Fixing printing of surrounding parentheses in "ltac:"."
Hugo Herbelin
2016-04-19
|
*
|
Fixing printing of surrounding parentheses in "ltac:".
Hugo Herbelin
2016-04-17
[prev]
[next]
Hugo Herbelin
Pierre-Marie Pédrot