From 123064557fce67e98f73ee56bb4aff534c9ceb85 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 12:43:12 +0100
Subject: Fix failing coqtops in gallina-extensions.rst

---
 doc/sphinx/language/gallina-extensions.rst | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 50a56f1d51..437b8e557e 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1970,6 +1970,10 @@ in :ref:`canonicalstructures`; here only a simple example is given.
 
          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.
@@ -2019,10 +2023,10 @@ or :g:`m` to the type :g:`nat` of natural numbers).
        Implicit Types m n : nat.
 
        Lemma cons_inj_nat : forall m n l, n :: l = m :: l -> n = m.
-
-       intros m n.
+       Proof. intros m n. Abort.
 
        Lemma cons_inj_bool : forall (m n:bool) l, n :: l = m :: l -> n = m.
+       Abort.
 
 .. cmdv:: Implicit Type @ident : @type
 
-- 
cgit v1.2.3