%=======================================================================
% 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,

}