aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Notations.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-04-25 14:49:18 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-05-28 09:38:36 -0400
commit9922c243e6d6a01d7308a6b1ce2aefd44d1b100e (patch)
treed9b6d953ffe673f6943827d8a95220d0e29a804e /theories/Init/Notations.v
parent0a2362cd8547bc073d60470c2a49174dd15634d0 (diff)
Add some more comments about sigma equalities
Forwards/backwards reasoning thoughts come from https://github.com/coq/coq/pull/385#discussion_r111008347
Diffstat (limited to 'theories/Init/Notations.v')
0 files changed, 0 insertions, 0 deletions