From 1fb883aaf4dc0b1111befd7a44395de76547c330 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 4 Dec 2013 15:50:12 +0100
Subject: Documentation of the Derive plugin.

I put it in a new chapter of the Addendum of the manual. Which is meant to be dedicated to plugins with short documentation.---
 Makefile.common                 | 2 +-
 doc/refman/Reference-Manual.tex | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/Makefile.common b/Makefile.common
index d74f143bd1..b13e828c4e 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -122,7 +122,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \
   Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
-  Setoid.v.tex Helm.tex Classes.v.tex )
+  Setoid.v.tex Helm.tex Classes.v.tex Misc.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 7b6c8ba3be..152bdb3eee 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -122,6 +122,7 @@ Options A and B of the licence are {\em not} elected.}
 \include{Polynom.v}%  = Ring
 \include{Nsatz.v}%
 \include{Setoid.v}% Tactique pour les setoides
+\include{Misc.v}
 %BEGIN LATEX
 \RefManCutCommand{ENDADDENDUM=\thepage}
 %END LATEX
-- 
cgit v1.2.3