coq/test-suite/ideal-features, branch master The formal proof system 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.
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 






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

Théo Zimmermann

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

629fbc743f8b5e7623a6834f19885b2e379cb782












Moving bug numbers to BZ# format in the test-suite.
2017-10-19T14:11:49+00:00

Théo Zimmermann

2017-10-19T14:04:20+00:00

fb1478d2cd59991e8d2fc2e07dacad505ef110b7

Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.





Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.







Ensuring all .v files end with a newline to make "sed -i" work better on them.
2017-08-21T16:29:07+00:00

Hugo Herbelin

2017-08-21T16:29:07+00:00

9dea4814ae928192e23764c09473501e2ecc9937












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

Pierre-Marie Pédrot

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

3e0334dd48b5d0b03046d0aff1a82867dc98d656












Update copyright headers.
2016-01-20T16:33:09+00:00

Maxime Dénès

2016-01-20T16:25:10+00:00

86f5c0cbfa64c5d0949365369529c5b607878ef8












Update headers.
2015-01-12T13:24:46+00:00

Maxime Dénès

2015-01-12T13:24:46+00:00

d90a5d4bfb05cd832b439044542a8c22ad5bd3ee












Updating headers.
2012-08-08T18:56:15+00:00

herbelin

2012-08-08T18:56:15+00:00

a234672e9d669397b40b59254c482f49007000df

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7





git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7







ZArith + other : favor the use of modern names instead of compat notations
2012-07-05T16:56:16+00:00

letouzey

2012-07-05T16:56:16+00:00

fc2613e871dffffa788d90044a81598f671d0a3b

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7





 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7