aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Loop.v
Commit message (Collapse)AuthorAge
* Allow loop notation to printGravatar Jason Gross2017-06-05
| | | | | | With help from Hugo at https://coq.inria.fr/bugs/show_bug.cgi?id=5581#c1 cc @andres-erbsen
* Add an only-parsing loop notationGravatar Jason Gross2017-06-02
|
* Add experimental loopsGravatar Jason Gross2017-06-02
Written via pair-programming with Andres.