aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Notations.v
Commit message (Expand)AuthorAge
* Clean up notations after bbv removalHEADmasterGravatar Benjamin Barenblat2019-04-26
* Add reserved notations for \inGravatar Jason Gross2019-03-05
* Add more reserved notationsGravatar Jason Gross2018-11-19
* Add more reserved notationsGravatar Jason Gross2018-11-01
* Actually fix the build for Coq 8.7Gravatar Jason Gross2018-09-17
* Reserve 'n notation in Notations.vGravatar Jason Gross2018-08-08
* Reserve ==, ===, ~=Gravatar Jason Gross2018-07-25
* Reserve ;;;, fix level of prefix # to not clash with infix #Gravatar Jason Gross2018-07-25
* Reserve a notatoin for ;;Gravatar Jason Gross2018-06-16
* Add more bind reserved notationsGravatar Jason Gross2018-05-31
* Backtrack on moving a notation to Notations.v, to fix conflictGravatar Jason Gross2018-05-06
* Fix notations to not conflict with bbvGravatar Jason Gross2018-05-06
* More reserved notationsGravatar Jason Gross2018-05-06
* Add another notationGravatar Jason Gross2018-05-06
* Fix a typo in last commitGravatar Jason Gross2018-05-06
* Add a reserved notation for #vGravatar Jason Gross2018-05-06
* Add another reserved notation for App_fstGravatar Jason Gross2018-03-21
* Add a file to parse taps with Coq notationsGravatar Jason Gross2018-02-14
* Add better levels / printing for bind notationsGravatar Jason Gross2018-01-16
* Add @@ infix notationGravatar Jason Gross2018-01-06
* Add some reserved notations for cps stuffGravatar Jason Gross2017-12-27
* Add reserved notation for infix @ for applicationGravatar Jason Gross2017-12-15
* Reserve a printing-only notation for function applicationGravatar Jason Gross2017-11-26
* Add reserved expr_let notationGravatar Jason Gross2017-11-26
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
* Add notationsGravatar Jason Gross2017-10-10
* Fix zrange notation levelsGravatar Jason Gross2017-06-12
* Reserve some more notationsGravatar Jason Gross2017-06-11
* Fix notation binding levels so types work in nletGravatar Jason Gross2017-05-14
* Add some reserved notationsGravatar Jason Gross2017-05-14
* Allow specifying type in nletGravatar Jason Gross2017-05-14
* Support destructuring dlet and sletGravatar Jason Gross2017-05-13
* Add reserved notationsGravatar Jason Gross2017-05-11
* Add for-loop combinatorGravatar Jason Gross2017-04-14
* Update display to not line-wrapGravatar Jason Gross2017-04-13
* Use r[_ ~> _] for range rather than b[_ ~> _]Gravatar Jason Gross2017-03-30
* Don't reserve '(max_bitwidth'Gravatar Jason Gross2017-03-28
* Add a notation for printingGravatar Jason Gross2017-03-28
* Add dlet_nd notationGravatar Jason Gross2017-03-01
* Factor things into BoundByCast.vGravatar Jason Gross2017-02-08
* Update notations from zetabaseGravatar Jason Gross2017-01-19
* Remove the Const constructor of exprfGravatar Jason Gross2017-01-19
* Add >>> reserved notationGravatar Jason Gross2017-01-09
* Fix compatibility with sigT notationGravatar Jason Gross2016-10-10
* Revert "Add a locked version of [let] with fewer reductions"Gravatar Jason Gross2016-09-22
* Add a form of Let_In that carries a proofGravatar Jason Gross2016-09-22
* Add a locked version of [let] with fewer reductionsGravatar Jason Gross2016-09-22
* Change [Let ... in ...] to [dlet ... in ...] (#67)Gravatar Jason Gross2016-09-19
* Util.Notations: change Let to match slet\Gravatar Andres Erbsen2016-09-18
* Add reserved notation for Let, change #Gravatar Jason Gross2016-09-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-29 16:12:37 +0000