diff options
| author | Pierre-Marie Pédrot | 2020-11-15 13:38:41 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-16 12:28:27 +0100 |
| commit | 3fe5f962d236448e78f55dd6761da173a30f8be4 (patch) | |
| tree | 81feffcbc7e7675080f96890be43c58720fb7d67 /doc/sphinx/proofs | |
| parent | 3c9908f9b7c73af2ad9c617b3ced424dca2fcb2e (diff) | |
Tentative fix for the refman.
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 485b92342d..510457fd0c 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -123,6 +123,10 @@ Programmable proof search .. example:: + .. coqtop:: none + + Set Warnings "-deprecated-hint-without-locality". + .. coqtop:: all Hint Resolve ex_intro : core. @@ -405,6 +409,10 @@ automatically created. .. example:: + .. coqtop:: none + + Set Warnings "-deprecated-hint-without-locality". + .. coqtop:: in Hint Extern 4 (~(_ = _)) => discriminate : core. @@ -419,7 +427,11 @@ automatically created. .. example:: - .. coqtop:: reset all + .. coqtop:: reset none + + Set Warnings "-deprecated-hint-without-locality". + + .. coqtop:: all Require Import List. Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. |