coq/test-suite/stm, branch master The formal proof system Remove the omega tactic and related options 2021-04-03T01:52:59+00:00 Jim Fehrle 2021-01-11T22:47:13+00:00 d3a51ac24244f586dfeff1a93b68cb084370534e 






Fixing typos - Part 3
2019-05-23T21:28:55+00:00

JPR

2019-05-23T21:28:55+00:00

d306f5428db0d034aea55d3f0699c67c1f296cc1












[test-suite] Improve test for async workers.
2019-02-08T17:24:11+00:00

Emilio Jesus Gallego Arias

2019-02-08T17:24:11+00:00

8276171d890360e9864d0e314f7ce4b12ba9040f












[stm] Filter some more arguments that shouldn't be sent to workers.
2019-02-08T10:02:16+00:00

Emilio Jesus Gallego Arias

2019-02-06T17:37:27+00:00

f828ca388911f66452c88d0e907331bf0a8a59cb

This fixes #9484 .





This fixes #9484 .







Merge PR #9223: Fix universe restriction in delayed mode.
2018-12-18T19:49:04+00:00

Pierre-Marie Pédrot

2018-12-18T19:49:04+00:00

2cad4dec40cef2aecb19c5a0e5a1368392be8d88












Restrict body universes in delayed mode.
2018-12-17T13:49:44+00:00

Gaëtan Gilbert

2018-12-14T13:00:14+00:00

bdd943063ccd1309654b545819964c7c20752314












Fix classification of Set Default Proof Mode.
2018-12-17T13:48:24+00:00

Gaëtan Gilbert

2018-12-14T12:29:06+00:00

b9f78d6b3da817de84e42eca90e3807004452046












Update the -compat flags
2018-10-02T18:45:40+00:00

Jason Gross

2018-10-02T18:45:00+00:00

3208a68e2c1b5f29fe33b54a66a2c361d3bfc531

Mostly via `dev/tools/update-compat.py --cur-version=8.9`

We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).

We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).





Mostly via `dev/tools/update-compat.py --cur-version=8.9`

We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).

We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).







Updating test-suite after Bracketing Last Introduction Pattern set by
2015-11-10T18:00:00+00:00

Hugo Herbelin

2015-11-10T17:43:07+00:00

f0ff590f380fb3d9fac6ebfdd6cfd7bf6874658e

default. Interestingly, there is an example where it makes the rest of
the proof less natural.

Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].

where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.

Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":

intros [|p1|p1]; [intros y|intros [|p2|p2] ..].





default. Interestingly, there is an example where it makes the rest of
the proof less natural.

Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].

where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.

Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":

intros [|p1|p1]; [intros y|intros [|p2|p2] ..].







Remove some outdated files and fix permissions.
2015-07-31T07:35:50+00:00

Guillaume Melquiond

2015-07-31T07:34:48+00:00

505eb0f0dae9b8a6ac810070d60916b67942b305