diff options
| author | Théo Zimmermann | 2019-02-16 16:03:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:11 +0100 |
| commit | b16cea4007e4286d596a46bce80815939bca271d (patch) | |
| tree | 3c4eab3e78c364e21fa88a6d610d14846547518c /doc/sphinx/language | |
| parent | ea8a9125a4e81e7c848cf53f1e34f534d359e832 (diff) | |
Using options abort and restart of coqtop directive in the manual.
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 6 |
2 files changed, 2 insertions, 10 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 963242ea72..c1eab8a970 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -264,17 +264,13 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. -.. coqtop:: in +.. coqtop:: in abort Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. -.. coqtop:: none - - Abort. - .. _datatypes: Datatypes diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 933f07674a..2f99368f48 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1967,14 +1967,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. - .. coqtop:: all + .. coqtop:: all abort Lemma is_law_S : is_law S. - .. coqtop:: none - - Abort. - .. note:: If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. |