1 files changed, 0 insertions, 152 deletions
diff --git a/doc/refman/coq-listing.tex b/doc/refman/coq-listing.tex
deleted file mode 100644
index c69c3b1b8..000000000
--- a/doc/refman/coq-listing.tex
+++ /dev/null
@@ -1,152 +0,0 @@
-%=======================================================================
-% Listings LaTeX package style for Gallina + SSReflect (Assia Mahboubi 2007)
-
-\lstdefinelanguage{SSR} {
-
-% Anything betweeen $ becomes LaTeX math mode
-mathescape=true,
-% Comments may or not include Latex commands
-texcl=false,
-
-
-% Vernacular commands
-morekeywords=[1]{
-From, Section, Module, End, Require, Import, Export, Defensive, Function,
-Variable, Variables, Parameter, Parameters, Axiom, Hypothesis, Hypotheses,
-Notation, Local, Tactic, Reserved, Scope, Open, Close, Bind, Delimit,
-Definition, Let, Ltac, Fixpoint, CoFixpoint, Add, Morphism, Relation,
-Implicit, Arguments, Set, Unset, Contextual, Strict, Prenex, Implicits,
-Inductive, CoInductive, Record, Structure, Canonical, Coercion,
-Theorem, Lemma, Corollary, Proposition, Fact, Remark, Example,
-Proof, Goal, Save, Qed, Defined, Hint, Resolve, Rewrite, View,
-Search, Show, Print, Printing, All, Graph, Projections, inside,
-outside, Locate, Maximal},
-
-% Gallina
-morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
-      match, with, end, as, in, return, let, if, is, then, else,
-      for, of, nosimpl},
-
-% Sorts
-morekeywords=[3]{Type, Prop},
-
-% Various tactics, some are std Coq subsumed by ssr, for the manual purpose
-morekeywords=[4]{
-         pose, set, move, case, elim, apply, clear,
-            hnf, intro, intros, generalize, rename, pattern, after,
-	    destruct, induction, using, refine, inversion, injection,
-         rewrite, congr, unlock, compute, ring, field,
-            replace, fold, unfold, change, cutrewrite, simpl,
-         have, gen, generally, suff, wlog, suffices, without, loss, nat_norm,
-            assert, cut, trivial, revert, bool_congr, nat_congr, abstract,
-	 symmetry, transitivity, auto, split, left, right, autorewrite},
-
-% Terminators
-morekeywords=[5]{
-         by, done, exact, reflexivity, tauto, romega, omega,
-         assumption, solve, contradiction, discriminate},
-
-
-% Control
-morekeywords=[6]{do, last, first, try, idtac, repeat},
-
-% Various symbols
-% For the ssr manual we turn off the prettyprint of formulas
-% literate=
-%	{->}{{$\rightarrow\,$}}2
-% 	{->}{{\tt ->}}3
-%	{<-}{{$\leftarrow\,$}}2
-% 	{<-}{{\tt <-}}2
-% 	{>->}{{$\mapsto$}}3
-% 	{<=}{{$\leq$}}1
-% 	{>=}{{$\geq$}}1
-% 	{<>}{{$\neq$}}1
-% 	{/\\}{{$\wedge$}}2
-% 	{\\/}{{$\vee$}}2
-% 	{<->}{{$\leftrightarrow\;$}}3
-% 	{<=>}{{$\Leftrightarrow\;$}}3
-% 	{:nat}{{$~\in\mathbb{N}$}}3
-%	{fforall\ }{{$\forall_f\,$}}1
-%	{forall\ }{{$\forall\,$}}1
-%	{exists\ }{{$\exists\,$}}1
-% 	{negb}{{$\neg$}}1
-% 	{spp}{{:*:\,}}1
-% 	{~}{{$\sim$}}1
-% 	{\\in}{{$\in\;$}}1
-% 	{/\\}{$\land\,$}1
-% 	{:*:}{{$*$}}2
-%	{=>}{{$\,\Rightarrow\ $}}1
-% 	{=>}{{\tt =>}}2
-% 	{:=}{{{\tt:=}\,\,}}2
-% 	{==}{{$\equiv$}\,}2
-% 	{!=}{{$\neq$}\,}2
-% 	{^-1}{{$^{-1}$}}1
-% 	{elt'}{elt'}1
-%       {=}{{\tt=}\,\,}2
-%       {+}{{\tt+}\,\,}2,
-literate=
-	{isn't }{{{\ttfamily\color{dkgreen} isn't }}}1,
-
-% Comments delimiters, we do turn this off for the manual
-%comment=[s]{(*}{*)},
-
-% Spaces are not displayed as a special character
-showstringspaces=false,
-
-% String delimiters
-morestring=[b]",
-morestring=[d]",
-
-% Size of tabulations
-tabsize=3,
-
-% Enables ASCII chars 128 to 255
-extendedchars=true,
-
-% Case sensitivity
-sensitive=true,
-
-% Automatic breaking of long lines
-breaklines=true,
-
-% Default style fors listings
-basicstyle=\ttfamily,
-
-% Position of captions is bottom
-captionpos=b,
-
-% Full flexible columns
-columns=[l]fullflexible,
-
-% Style for (listings') identifiers
-identifierstyle={\ttfamily\color{black}},
-% Note : highlighting of Coq identifiers is done through a new
-% delimiter definition through an lstset at the begining of the
-% document. Don't know how to do better.
-
-% Style for declaration keywords
-keywordstyle=[1]{\ttfamily\color{dkviolet}},
-
-% Style for gallina keywords
-keywordstyle=[2]{\ttfamily\color{dkgreen}},
-
-% Style for sorts keywords
-keywordstyle=[3]{\ttfamily\color{lightblue}},
-
-% Style for tactics keywords
-keywordstyle=[4]{\ttfamily\color{dkblue}},
-
-% Style for terminators keywords
-keywordstyle=[5]{\ttfamily\color{red}},
-
-
-%Style for iterators
-keywordstyle=[6]{\ttfamily\color{dkpink}},
-
-% Style for strings
-stringstyle=\ttfamily,
-
-% Style for comments
-commentstyle=\rmfamily,
-
-}