index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
output
/
Notations3.v
Age
Commit message (
Expand
)
Author
2017-09-12
Fixing a bug of recursive notations introduced in dfdaf4de.
Hugo Herbelin
2017-08-29
Adding a test for #5569 (warning about skipping spaces).
Hugo Herbelin
2017-08-29
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-07-26
Adding support for recursive notations of the form "x , .. , y , z".
Hugo Herbelin
2017-06-08
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-05-31
Fixing a too lax constraint for finding recursive binder part of a notation.
Hugo Herbelin
2017-05-20
Added a test for #4765 (an example of printing abbreviation with binders).
Hugo Herbelin
2017-05-17
Fixing bug #5526,allow nonlinear variables in Notation patterns
Paul Steckler
2016-07-19
Taking into account binding patterns when agglutinating sequences of binders.
Hugo Herbelin
2016-07-19
Notations: fixing multiple binders used as terms in reverse order.
Hugo Herbelin
2016-07-18
A new step on using alpha-conversion in printing notations.
Hugo Herbelin
2016-07-17
Partial fix to #4592 (notation requiring alpha-conversion for printing).
Hugo Herbelin
2016-07-17
More examples of recursive notations, with emphasis in reference manual.
Hugo Herbelin
2016-07-17
Fixing a bug in recognizing a recursive pattern of notations
Hugo Herbelin
2016-07-17
Fixing interpretation of notations w/ opposite instances of a recursive pattern.
Hugo Herbelin
2016-07-17
Fixing printing of notations with several instances of a recursive pattern.
Hugo Herbelin
