Support locality attributes for Hint Rewrite (including export)2021-01-18T12:08:17+00:00Gaëtan Gilbert2021-01-07T12:55:23+00:004419a101a4f5a108be90cf4e420f0b6961e6caac
We deprecate unspecified locality as was done for Hint.
Close #13724
We deprecate unspecified locality as was done for Hint.
Close #13724
Modify Structures/OrderedType.v to compile with -mangle-names2021-01-08T22:26:10+00:00Jasper Hugunin2021-01-08T22:26:10+00:0006c816527a26a9e9e09601b67c128b381c4bd2af
Modify Structures/DecidableType.v to compile with -mangle-names2021-01-08T22:14:58+00:00Jasper Hugunin2021-01-08T22:14:58+00:0026f6b7ada0007fece59b0ff054ac13ec733dfcf8
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.
Adapting theories to unused pattern-matching variable warning.2020-10-05T14:19:12+00:00Hugo Herbelin2020-08-18T20:49:00+00:002fb42ce6b9b74a2c5f66e9fa9cb16745cdb85687
Modify Structures/GenericMinMax.v to compile with -mangle-names2020-08-25T20:53:32+00:00Jasper Hugunin2020-08-25T20:10:40+00:00c16e4c23e6591aace243c5503ce70e99d3c0569d
Modify Structures/OrdersFacts.v to compile with -mangle-names2020-08-25T20:53:32+00:00Jasper Hugunin2020-08-25T20:09:21+00:0032240c45be0835b6b32eec6f85743fa3c4c15537
Modify Structures/OrdersTac.v to compile with -mangle-names2020-08-25T20:53:32+00:00Jasper Hugunin2020-08-25T20:07:08+00:002d01a4794e4a684d9868ab7e7e58966a12161de7
Modify Structures/Orders.v to compile with -mangle-names2020-08-25T20:53:32+00:00Jasper Hugunin2020-08-25T20:05:49+00:0017ed93c2caadfcf3a2aee8f2b9683191063b2951