coq/theories/FSets, branch master The formal proof system 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
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.
Adapting theories to unused pattern-matching variable warning. 2020-10-05T14:19:12+00:00 Hugo Herbelin 2020-08-18T20:49:00+00:00 2fb42ce6b9b74a2c5f66e9fa9cb16745cdb85687 






Fixing #11903: Fixpoints not truly recursive in standard library.
2020-05-01T21:17:27+00:00

Hugo Herbelin

2020-04-19T11:00:09+00:00

df8df4637dfb4106854554cc2ac94b4fdd565e80

There was also a non truly recursive in the doc.





There was also a non truly recursive in the doc.







Avoiding using a fixed introduction name in Ltac code of stdlib.
2020-04-03T18:33:27+00:00

Hugo Herbelin

2020-03-22T11:30:55+00:00

aa889ee516453af65bd74ffedf8ec3761f97eb43












firstorder: default tactic is “auto with core”
2020-03-19T07:05:07+00:00

Vincent Laporte

2020-01-18T19:35:42+00:00

e138fbf1e1cd95bfae05e17074f94a1ebde2edf8












[stdlib] Remove a few `auto with *`
2020-03-19T07:05:02+00:00

Vincent Laporte

2020-03-10T12:02:15+00:00

daad81ddd72f4a8892b683d4f2b72345ff0bb84f












Update headers in the whole code base.
2020-03-18T11:15:43+00:00

Théo Zimmermann

2020-03-18T11:14:26+00:00

a99776e10e0b2198d2b811ad82631111fb450f8a

Add headers to a few files which were missing them.





Add headers to a few files which were missing them.







FSetEqProperties: do not use “omega”
2019-10-22T06:39:10+00:00

Vincent Laporte

2019-10-10T13:56:46+00:00

4af9a79457fc265b1696de2b1fa1018ef12c986a












FSets: do not use “omega”
2019-10-22T06:38:20+00:00

Vincent Laporte

2019-10-10T12:14:55+00:00

abdf4058321e3767421cd0c30d8f4fc63e0518e3