index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
Notations4.v
Age
Commit message (
Expand
)
Author
2019-05-10
Use Print Custom Grammar to inspect custom entries
Jasper Hugunin
2019-04-29
Revert #8187
Vincent Laporte
2019-04-29
Revert #9249
Vincent Laporte
2019-02-19
Notations: Fixing a printing bug with patterns.
Hugo Herbelin
2019-02-04
Primitive integers
Maxime Dénès
2019-01-25
Notations: Removing useless parentheses on abbrevs for prefix of an application.
Hugo Herbelin
2018-12-25
Fixing printing bug due to using equality ill-checking hash key of kernel name.
Hugo Herbelin
2018-12-04
Giving to type_scope a softer role in printing.
Hugo Herbelin
2018-12-04
Printing priority to most recent notation in case of non-open scopes with delim.
Hugo Herbelin
2018-12-04
Using scope for printing: more tests.
Hugo Herbelin
2018-12-04
Fixing #8551 (missing delimiters when notation exists both lonely and in scope).
Hugo Herbelin
2018-12-04
Selecting which notation to print based on current stack of scope.
Hugo Herbelin
2018-11-20
Notations: Trying using a notation with or w/o removal of coercions.
Hugo Herbelin
2018-10-31
Notations: fixing a bug with abbreviations in custom entries.
Hugo Herbelin
2018-07-29
Adding support for custom entries in notations.
Hugo Herbelin
