diff options
| author | Vincent Laporte | 2018-10-24 11:09:01 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-24 11:54:30 +0000 |
| commit | a95c781dadd2b4aa5a6b715cfc7238e761a807fc (patch) | |
| tree | 4f069c4d873f397acb172cb164ede18f63ea457e /doc | |
| parent | 3dd46db42776f9be448454b2ddf556663295abd8 (diff) | |
[Manual] Fix layout of a list
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 52609546d5..e976396950 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3756,9 +3756,10 @@ which the function is supplied: :name: congr This tactic: -+ checks that the goal is a Leibniz equality -+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints. -+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. + + + checks that the goal is a Leibniz equality; + + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. The goal can be a non dependent product ``P -> Q``. In that case, the system asserts the equation ``P = Q``, uses it to solve the goal, and |