coq/theories/Classes, branch masterThe formal proof systemRemove the :> type cast2021-03-30T16:51:56+00:00Jim Fehrle2021-03-07T18:15:11+00:00eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf
Modify Classes/SetoidDec.v to compile with -mangle-names2021-01-08T22:01:55+00:00Jasper Hugunin2021-01-08T22:01:55+00:008241077c681bb48a0b413e4ee68961f0684b0294
Modify Classes/SetoidClass.v to compile with -mangle-names2021-01-08T22:00:50+00:00Jasper Hugunin2021-01-08T22:00:50+00:00e2850002db0271aff914c6a81d17354991b0d5cb
Modify Classes/EquivDec.v to compile with -mangle-names2021-01-08T20:42:47+00:00Jasper Hugunin2021-01-08T20:42:47+00:007dd5f0cc776f0a79b3852cd1ed30fa0edab17a73
Modify Classes/DecidableClass.v to compile with -mangle-names2020-12-16T04:51:29+00:00Jasper Hugunin2020-12-16T04:51:29+00:0029c881414cf1ae7c6c882c1285f72b5d5cba1b4e
Modify Classes/CEquivalence.v to compile with -mangle-names2020-12-16T04:49:26+00:00Jasper Hugunin2020-12-16T04:49:26+00:00511a81ab5826ecf2f0eae2447da7a3f83b660003
Catch up to where I was last time.2020-12-16T01:40:23+00:00Jasper Hugunin2020-12-16T01:40:23+00:0003ebf8633afb5dce97b957b2b5928f0ecac8f804
Many of the changes are a consequence of coq/coq#13132.
Many of the changes are a consequence of coq/coq#13132.
Convert auto chapter to prodn2020-11-24T20:06:54+00:00Jim Fehrle2020-09-13T03:54:22+00:00b1846e859091e24db1210be53f9193aa3aedb4d9
Merge PR #13384: Warn on hints without an explicit locality2020-11-16T16:26:41+00:00coqbot-app[bot]2020-11-16T16:26:41+00:00af96434d2991b9f01f6cd3963ed114b57e40792f
Reviewed-by: Zimmi48
Reviewed-by: Zimmi48
Explicitly annotate all hint declarations of the standard library.2020-11-16T11:28:27+00:00Pierre-Marie Pédrot2020-11-14T16:55:07+00:0068cd077344ce37db1a601079dbc4fdcae6c8d41f
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.