coq/theories/Strings, branch master The formal proof system Ascii: add leb and ltb 2020-12-03T18:06:20+00:00 Yishuai Li 2020-09-24T07:41:37+00:00 aab8634bcda7829004c369644e9d4600692913f0 






Merge PR #13173: Lint stdlib with -mangle-names #4
2020-11-09T08:07:27+00:00

coqbot-app[bot]

2020-11-09T08:07:27+00:00

fcc82eaf6054cce65821fafafedd329dab732994

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







Modify Strings/String.v to compile with -mangle-names
2020-10-12T02:05:14+00:00

Jasper Hugunin

2020-10-09T23:38:52+00:00

3c5ff2175d0711da2dca1259b953f308cd5d82ae












Modify Strings/Ascii.v to compile with -mangle-names
2020-10-12T02:05:14+00:00

Jasper Hugunin

2020-10-09T23:33:49+00:00

5a3d6f1d2c193be514e610779b80829eef4fe4a8












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












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.







Avoid hardcoded paths in extraction
2020-01-08T14:07:15+00:00

Maxime Dénès

2019-12-04T12:52:39+00:00

9705ff0d0673b9c2df8fa08c8aab01d2c40bc8f6












Update headers of files that were stuck on older headers.
2019-06-17T16:08:32+00:00

Théo Zimmermann

2019-06-06T09:22:08+00:00

35472e260eb609438eda7de9744a104ef8ef906d

Most of these files were introduced after #6543 but used older headers
copied from somewhere else.





Most of these files were introduced after #6543 but used older headers
copied from somewhere else.







Update ml-style headers to new year.
2019-06-17T16:08:32+00:00

Théo Zimmermann

2019-06-06T09:22:08+00:00

42e09b6d888a29cc6273b8e77d5f9a2e5582abc4












Modifying theories to preferably use the "[= ]" syntax, and,
2019-05-25T13:36:59+00:00

Hugo Herbelin

2019-05-23T15:27:08+00:00

71110a218f69a69010adde2f296e4022ef94b755

sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>





sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>