coq/theories/Sorting, branch master The formal proof system 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
add results on count_occ 2021-01-29T21:25:43+00:00 Olivier Laurent 2021-01-29T07:52:57+00:00 19a8c5723625dbf49890f17858d330eb2f5ba94d 






Modify Sorting/Sorted.v to compile with -mangle-names
2021-01-08T20:48:29+00:00

Jasper Hugunin

2021-01-08T20:48:29+00:00

d18df3740d23b868cbd120dd449d276cd748dd35












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.







Additional statements about List.repeat
2020-08-12T10:06:49+00:00

Olivier Laurent

2020-08-07T16:55:46+00:00

94bb6fa0152ea61661f2e5d990f8d46cbdcdf9cf

Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>





Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>







Declare more Permutation instances as Global
2020-05-08T14:23:16+00:00

Olivier Laurent

2020-04-25T22:18:04+00:00

354582c02622ce99b61b24471981e45a14a372a4












Merge PR #12171: [stdlib] [list] Symmetry in conclusions of map_eq_cons and map_eq_app
2020-05-06T21:03:27+00:00

Hugo Herbelin

2020-05-06T21:03:27+00:00

325a644b3f5a5f8c1a86191004576e7c763ae9f3

Reviewed-by: anton-trunov
Reviewed-by: herbelin





Reviewed-by: anton-trunov
Reviewed-by: herbelin







consistency with Permutation
2020-05-03T09:34:00+00:00

Olivier Laurent

2020-05-03T09:34:00+00:00

3b06585b1ab4c0e77afcdccf584335b7b8050697












Symmetry in conclusions of List.map_eq_*
2020-04-30T11:54:34+00:00

Olivier Laurent

2020-04-24T15:07:09+00:00

245b58ac8b6dda26005ae998e5d2cf61a069711c

  allow simplified iterated applications





  allow simplified iterated applications







Merge PR #12120: Fixing #12119 : remove useless hypothesis in NoDup_Permutation_bis
2020-04-23T19:53:05+00:00

Hugo Herbelin

2020-04-23T19:53:05+00:00

a50cb07b1e7d161491e2c1d48fd3525b29397524

Reviewed-by: herbelin





Reviewed-by: herbelin