diff options
| author | Clément Pit-Claudel | 2019-02-19 12:52:04 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-02-19 12:52:04 -0500 |
| commit | c39482e63aacf47359d8f76c44c2d851c7cfb9a5 (patch) | |
| tree | b57047087583c8d991aed295bfee679bf54fd85a /doc/sphinx/language | |
| parent | c3cc72ccf586703ed009a8bdd5df8d40b0384ab2 (diff) | |
| parent | 499491f8efd3a02dacb64c779edc246510b1d35f (diff) | |
Merge PR #9501: Sphinx: fail when a command fails + other stuff
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
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 d2fd08536a..25f983ac1e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1962,14 +1962,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. |