diff options
| author | Cyril Cohen | 2020-08-10 19:54:48 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-08-10 19:54:48 +0200 |
| commit | d5a8bdc8f67b691dd39a27a9fe07a026d998fda3 (patch) | |
| tree | d7c9a94c9fa3edb09c11fd1705654796b6ddda59 /doc | |
| parent | ef08abec26c2f0017d1136870f8f99144e579538 (diff) | |
| parent | 0aa3f871051c737192f9a19b79957b32b6ecafea (diff) | |
Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)
Reviewed-by: CohenCyril
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 6 |
2 files changed, 15 insertions, 5 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b4b80ca21..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1211,6 +1211,8 @@ The move tactic. :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. +.. _the_case_tactic_ssr: + The case tactic ``````````````` @@ -1235,7 +1237,17 @@ The case tactic x = 1 -> y = 2 -> G. - Note also that the case of |SSR| performs :g:`False` elimination, even + The :tacn:`case` can generate the following warning: + + .. warn:: SSReflect: cannot obtain new equations out of ... + + The tactic was run on an equation that cannot generate simpler equations, + for example `x = 1`. + + The warning can be silenced or made fatal by using the :opt:`Warnings` option + and the `spurious-ssr-injection` key. + + Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 25c4de7389..c5fab0983f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2227,9 +2227,6 @@ and an explanation of the underlying technique. then :n:`injection @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - .. exn:: Nothing to do, it is an equality between convertible terms. :undocumented: @@ -2237,7 +2234,8 @@ and an explanation of the underlying technique. :undocumented: .. exn:: Nothing to inject. - :undocumented: + + This error is given when one side of the equality is not a constructor. .. tacv:: injection @num |