coq/theories/Numbers/Cyclic/ZModulo, branch master The formal proof system 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.
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.
Numbers.Cyclic: use “lia” rather than “omega” 2019-10-30T08:37:42+00:00 Vincent Laporte 2019-10-29T15:50:17+00:00 cd686690618713fca47de35ce8fcec47fc10391c 






[stdlib] Remove deprecated module Zlogarithm
2019-07-26T09:11:29+00:00

Vincent Laporte

2019-03-20T17:01:56+00:00

2f57090a48768f5cdc386110b0d21a620fe67d05












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>







Deprecate hint declaration/removal with no specified database
2018-11-14T07:53:03+00:00

Maxime Dénès

2018-11-13T15:39:54+00:00

eeb1d861551e25c6a92721334b3c9f36b7ebb012

Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).





Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).







Update headers following #6543.
2018-02-27T16:57:50+00:00

Théo Zimmermann

2018-02-27T16:02:31+00:00

629fbc743f8b5e7623a6834f19885b2e379cb782












Bump year in headers.
2017-07-04T12:20:57+00:00

Pierre-Marie Pédrot

2017-07-04T12:19:44+00:00

3e0334dd48b5d0b03046d0aff1a82867dc98d656












BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)
2017-06-13T08:30:29+00:00

Pierre Letouzey

2017-03-22T10:24:27+00:00

295107103aaa86db8a31abb0e410123212648d45

 See now https://github.com/coq/bignums
 Int31 is still in the stdlib.
 Some proofs there has be adapted to avoid the need for BigNumPrelude.





 See now https://github.com/coq/bignums
 Int31 is still in the stdlib.
 Some proofs there has be adapted to avoid the need for BigNumPrelude.