From f3bb625fb2d118168042b97162e1ece1bda4a039 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 19 Jul 2017 18:20:37 +0200
Subject: Removing testing unsupported Next.

---
 test-suite/coqdoc/bug5648.html.out | 7 -------
 test-suite/coqdoc/bug5648.tex.out  | 8 --------
 test-suite/coqdoc/bug5648.v        | 5 -----
 3 files changed, 20 deletions(-)

(limited to 'test-suite/coqdoc')

diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out
index f602e9859..06789c1c1 100644
--- a/test-suite/coqdoc/bug5648.html.out
+++ b/test-suite/coqdoc/bug5648.html.out
@@ -40,13 +40,6 @@
 &nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> =&gt; 6<br/>
 &nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> =&gt; 7<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
-
-<br/>
-<span class="id" title="keyword">Ltac</span> <span class="id" title="keyword">Next</span> := <span class="id" title="var">easy</span>.<br/>
-
-<br/>
-<span class="id" title="keyword">Lemma</span> <a name="yes"><span class="id" title="lemma">yes</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
-<span class="id" title="keyword">Proof</span>. <span class="id" title="keyword">Next</span>. <span class="id" title="keyword">Qed</span>.<br/>
 </div>
 </div>
 
diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out
index bb4c12be7..b0b732eff 100644
--- a/test-suite/coqdoc/bug5648.tex.out
+++ b/test-suite/coqdoc/bug5648.tex.out
@@ -45,13 +45,5 @@
 \ensuremath{|} \coqref{Coqdoc.bug5648.Proof}{\coqdocconstructor{Proof}} \ensuremath{\Rightarrow} 7\coqdoceol
 \coqdocindent{1.00em}
 \coqdockw{end}.\coqdoceol
-\coqdocemptyline
-\coqdocnoindent
-\coqdockw{Ltac} \coqdockw{Next} := \coqdocvar{easy}.\coqdoceol
-\coqdocemptyline
-\coqdocnoindent
-\coqdockw{Lemma} \coqdef{Coqdoc.bug5648.yes}{yes}{\coqdoclemma{yes}} : \coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}.\coqdoceol
-\coqdocnoindent
-\coqdockw{Proof}. \coqdockw{Next}. \coqdockw{Qed}.\coqdoceol
 \end{coqdoccode}
 \end{document}
diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v
index 353ecc49a..9b62dd1e1 100644
--- a/test-suite/coqdoc/bug5648.v
+++ b/test-suite/coqdoc/bug5648.v
@@ -17,8 +17,3 @@ Definition d x :=
   | P => 6
   | Proof => 7
   end.
-
-Ltac Next := easy.
-
-Lemma yes : True.
-Proof. Next. Qed.
-- 
cgit v1.2.3