coq/theories/Program, branch master The formal proof system Remove the :> type cast 2021-03-30T16:51:56+00:00 Jim Fehrle 2021-03-07T18:15:11+00:00 eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf 






Merge PR #13730: Lint stdlib with -mangle-names #6
2021-03-19T07:49:21+00:00

coqbot-app[bot]

2021-03-19T07:49:21+00:00

be64fe07ec2bcf5177bb227813d8f896ef00c265

Reviewed-by: anton-trunov





Reviewed-by: anton-trunov







Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)
2021-01-26T11:08:28+00:00

coqbot-app[bot]

2021-01-26T11:08:28+00:00

1a84bed789697ff9b4f5c70dec3c732cdbbdbce0

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48





Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48







Remove the Hide Obligations flag
2021-01-25T18:01:22+00:00

Jim Fehrle

2021-01-19T05:22:52+00:00

7ea0db435910c2db2a9ae4cadfd54f49f3640b62












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







Modify Program/Subset.v to compile with -mangle-names
2021-01-08T20:38:47+00:00

Jasper Hugunin

2021-01-08T20:38:47+00:00

76cbd4afbeb13d97852e97e805c0e1890eae1d6c












Modify Program/Wf.v to compile with -mangle-names
2020-12-16T04:59:23+00:00

Jasper Hugunin

2020-12-16T04:59:23+00:00

cd3d7e1384e2b6d929ad4d048810beb3e42f8a98












Adapting standard library, doc and test suite to ident->name renaming.
2020-11-22T12:28:40+00:00

Hugo Herbelin

2020-03-17T10:16:09+00:00

df8b5c7d83ad6e88af34d29bcc32c85bd42c2712












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.







Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-free
2020-11-13T06:04:59+00:00

Li-yao Xia

2020-11-13T04:35:45+00:00

e3a6e5f16e91e4b79a52bf11301db02211c74528