coq/test-suite/complexity, branch master

[micromega] Updated test-suite

2020-11-18T08:49:22+00:00

Moved bug_13227.v to complexity/bug_13227_i.v

CReal: changed epsilon for modulus of convergence from 1/n to 2^z

2020-06-09T08:19:17+00:00

Replace QSeqEquiv by QCauchySeq, simplify proofs.

2020-04-30T21:21:29+00:00

Force Cauchy modulus equal to identity, make division transparent

Fix test

constructive square root

2020-04-26T13:20:47+00:00

Convert into a performance test

Put time bound at the beginning of file

Add Time command in the test

Fix test-suite fo non maximal implicit arguments

2020-01-07T09:11:21+00:00

Relax the pattern complexity test

2019-11-28T06:23:36+00:00

c.f. discussion at
https://github.com/coq/coq/pull/11177#issuecomment-559139477

Update test-suite/complexity/pattern.v

2019-11-26T18:27:56+00:00

Co-Authored-By: Hugo Herbelin

Add a complexity test for `pattern`

2019-11-25T05:47:39+00:00

This is to hopefully prevent regressions on
https://github.com/coq/coq/issues/11150 and
https://github.com/coq/coq/issues/6502.

[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

2019-01-30T12:41:08+00:00

This PR deprecates the use of `coqtop` as a compiler.

There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.

We adapt the documentation and adapt the test-suite.

Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.

The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.

Change Implicit Arguments to Arguments in test-suite

2018-03-31T00:48:17+00:00