coq/doc/sphinx/proofs/automatic-tactics, 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 






Convert 2nd part of rewriting chapter to prodn
2021-03-08T19:48:20+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

0d33024ff79c38d52fde49e23d0e45d9c22eefbe












Infrastructure for fine-grained debug flags
2021-02-24T14:09:15+00:00

Maxime Dénès

2020-10-15T13:31:51+00:00

068031ff7da092c1e2d35db27d713b9606960c42












Improve wording for #13384
2021-01-21T20:08:47+00:00

Jim Fehrle

2021-01-21T20:02:49+00:00

56578a246e6b13d539fd6b0f54f7e06c641fd847












Support locality attributes for Hint Rewrite (including export)
2021-01-18T12:08:17+00:00

Gaëtan Gilbert

2021-01-07T12:55:23+00:00

4419a101a4f5a108be90cf4e420f0b6961e6caac

We deprecate unspecified locality as was done for Hint.

Close #13724





We deprecate unspecified locality as was done for Hint.

Close #13724







Convert rewriting and proof-mode chapters to prodn
2020-12-30T19:48:37+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

e02120ed6580733db2276f0c11b4f432ea670ee3












Convert auto chapter to prodn
2020-11-24T20:06:54+00:00

Jim Fehrle

2020-09-13T03:54:22+00:00

b1846e859091e24db1210be53f9193aa3aedb4d9












Document the new warning.
2020-11-16T11:28:27+00:00

Pierre-Marie Pédrot

2020-11-15T16:40:33+00:00

4f28dd46d4bfce732693d6904f80e25b53d4fb2a












Tentative fix for the refman.
2020-11-16T11:28:27+00:00

Pierre-Marie Pédrot

2020-11-15T12:38:41+00:00

3fe5f962d236448e78f55dd6761da173a30f8be4












Document the new export locality for the remaining hint commands.
2020-11-15T15:05:56+00:00

Pierre-Marie Pédrot

2020-11-15T14:30:28+00:00

7e55f4813d5173d659482a6899c3f97c5346a682