coq/theories/Lists, branch master The formal proof system remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, Setoid 2021-03-26T08:15:49+00:00 Andrej Dudenhefner 2021-03-23T18:20:18+00:00 d7ccf45bbb1b73006c5804bcfc18bb3f6f7c90fd fix unexpectedly broken MSetGenTree.v add changelog entry 
fix unexpectedly broken MSetGenTree.v
add changelog entry
add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat 2021-03-23T08:21:42+00:00 Andrej Dudenhefner 2021-03-23T07:01:14+00:00 680ffd88630ac7f630533ce33d19200b8669f34a 






Merge PR #13804: [stdlib] [List] Add results about count_occ
2021-03-23T08:00:38+00:00

coqbot-app[bot]

2021-03-23T08:00:38+00:00

7c9bb01b485cb3fd4b997125fbe2e4acb735054f

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







Merge PR #13730: Lint stdlib with -mangle-names #6
2021-03-19T07:49:21+00:00

coqbot-app[bot]

2021-03-19T07:49:21+00:00

be64fe07ec2bcf5177bb227813d8f896ef00c265

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







add results on count_occ
2021-01-29T21:25:43+00:00

Olivier Laurent

2021-01-29T07:52:57+00:00

19a8c5723625dbf49890f17858d330eb2f5ba94d












Support locality attributes for Hint Rewrite (including export)
2021-01-18T12:08:17+00:00

Gaëtan Gilbert

2021-01-07T12:55:23+00:00

4419a101a4f5a108be90cf4e420f0b6961e6caac

We deprecate unspecified locality as was done for Hint.

Close #13724





We deprecate unspecified locality as was done for Hint.

Close #13724







Modify Lists/SetoidList.v to compile with -mangle-names
2021-01-08T21:57:51+00:00

Jasper Hugunin

2021-01-08T21:57:51+00:00

d68d5d35e529cf6f7a9ef0e7639c92dd9b58540c

I used `match goal` a lot to access hypotheses without knowing their
name.





I used `match goal` a lot to access hypotheses without knowing their
name.







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.







Modify Lists/List.v to compile with -mangle-names
2020-09-16T20:23:13+00:00

Jasper Hugunin

2020-09-13T04:00:34+00:00

862a5b352e784fff9f1a9bde5ac3b887403ece57












Add iff variants for other list lemmas
2020-09-07T05:53:55+00:00

Edward Wang

2020-04-14T06:02:28+00:00

d79c6b1de2a5b0efbe4d2e2c75b4a7c587df6767