coq/theories/Logic, branch master The formal proof system Typo in ChoiceFacts. 2021-04-06T15:40:53+00:00 Hugo Herbelin 2021-03-16T10:48:57+00:00 4e28d88de719711a608389a02f9358182eec5235 






Standardizing spacing for {| ... |} in two files.
2021-04-06T15:40:53+00:00

Hugo Herbelin

2020-10-15T22:56:00+00:00

70751719b5adadaa384a18c80cc85a6582c12f4a












Modify Logic/ProofIrrelevanceFacts.v to compile with -mangle-names
2021-01-08T20:37:04+00:00

Jasper Hugunin

2021-01-08T20:37:04+00:00

afed8dcf54d7a9e8e8ac04e4ec2de1784270e2e4












Modify Logic/JMeq.v to compile with -mangle-names
2020-12-16T05:00:29+00:00

Jasper Hugunin

2020-12-16T05:00:29+00:00

ef7dbd83b583abf08f162e343250507ad74744a1












Modify Logic/FunctionalExtensionality.v to compile with -mangle-names
2020-12-16T04:53:29+00:00

Jasper Hugunin

2020-12-16T04:53:29+00:00

c53cd878c8291690d8799c0dd5f6af20534b0cbc












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.







Modify Logic/Eqdep_dec.v to compile with -v
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-13T00:06:09+00:00

52388892ae3bb7d071932947590ec9b09e12f7ce












Modify Logic/EqdepFacts.v to compile with -mangle-names
2020-09-16T19:46:57+00:00

Jasper Hugunin

2020-09-12T23:52:57+00:00

fb1405e9ef9d8d061af6ba9188764911f28f2b27












UIP in SProp
2020-07-01T11:06:22+00:00

Gaëtan Gilbert

2019-06-13T13:39:43+00:00

2ded4c25e532c5dfca0483c211653768ebed01a7