coq/theories/ssr, branch master The formal proof system Enable canonical `fun _ => _` projections. 2021-04-22T07:16:22+00:00 Jan-Oliver Kaiser 2020-05-14T15:08:20+00:00 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 






Backport ssrbool lemmas from MathComp 1.12.0
2020-11-29T13:41:21+00:00

Kazuhiko Sakaguchi

2020-11-26T17:34:35+00:00

86a3d1a4c742a273414c98f6a8b1a99f0d081a98












Fixing [dup] and [swap]
2020-11-24T16:03:31+00:00

Cyril Cohen

2020-11-23T16:55:27+00:00

5eb18289189a8a3d71086b12998e85d651970b28












Adapting standard library, doc and test suite to ident->name renaming.
2020-11-22T12:28:40+00:00

Hugo Herbelin

2020-03-17T10:16:09+00:00

df8b5c7d83ad6e88af34d29bcc32c85bd42c2712












[doc] [ssr] fix documentation of reflect
2020-11-20T09:14:21+00:00

Enrico Tassi

2020-11-20T09:14:21+00:00

fe56bc97653123d24631b0f9ed2e100259202099












Explicitly annotate all hint declarations of the standard library.
2020-11-16T11:28:27+00:00

Pierre-Marie Pédrot

2020-11-14T16:55:07+00:00

68cd077344ce37db1a601079dbc4fdcae6c8d41f

By default Coq stdlib warnings raise an error, so this is really required.





By default Coq stdlib warnings raise an error, so this is really required.







Intro pattern extensions for dup, swap and apply
2020-11-06T11:02:43+00:00

Cyril Cohen

2020-11-06T10:32:17+00:00

79c45ec7696923c9d2867b094ca30d6af142dbc8












Splitting ssrbool's multi-printing notations into parsing and printing.
2020-10-10T20:34:24+00:00

Hugo Herbelin

2020-08-30T13:10:53+00:00

2a50e04a58c97cf8a973b6e15ba5de326f3366e5

This is in anticipation of a model with an explicit difference between
a parsing-printing notation and the pair of only-parsing notation +
only-printing notation.





This is in anticipation of a model with an explicit difference between
a parsing-printing notation and the pair of only-parsing notation +
only-printing notation.







address comments and fixups
2020-08-25T21:32:04+00:00

Reynald Affeldt

2020-08-25T14:42:09+00:00

40140bfc872b104d184ba05a85f6ce918559a6ba












fix notation-incompatible-format warnings
2020-08-25T14:07:15+00:00

Reynald Affeldt

2020-08-25T14:07:15+00:00

bfd384ed5f7af818f6b893b50d0f8de49477c144

(mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)





(mathcomp commit 1bbfe3429a07bee2478fd15adf45b982fdfb5d2b)