%=======================================================================
% Définit le style ssr Gallina pour les listings (Assia Mahboubi 2007)

\lstdefinelanguage{grey} {

% Anything betweeen $ becomes LaTeX math mode
mathescape=true,						
% Comments may or not include Latex commands
texcl=false,

% Vernacular commands
morekeywords=[1]{
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, About},

% Gallina
morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
      match, with, end, as, in, return, let, if, is, then, else,
      for, of, nosimpl, at},

% 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, suff, wlog, suffices, without, loss, nat_norm,
            assert, cut, trivial, revert, bool_congr, nat_congr,
	 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},

literate=
	{isn't }{{{\ttfamily\color{dkgreen} isn't }}}1
	{===}{{{\color{dkgrey}===}}}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\color{dkgrey},

% Position of captions is bottom
captionpos=b,							

% Full flexible columns 
columns=[l]fullflexible,

% Style for (listings') identifiers
identifierstyle={\ttfamily\color{dkgrey}},
% 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{dkgrey}},

% Style for gallina keywords
keywordstyle=[2]{\ttfamily\color{dkgrey}},

% Style for sorts keywords
keywordstyle=[3]{\ttfamily\color{dkgrey}},

% Style for tactics keywords
keywordstyle=[4]{\ttfamily\color{dkgrey}},

% Style for terminators keywords
keywordstyle=[5]{\ttfamily\color{dkgrey}},


%Style for iterators
keywordstyle=[6]{\ttfamily\color{dkgrey}},

% Style for strings
stringstyle=\ttfamily\color{dkgrey},

% Style for comments
commentstyle=\ttfamily\color{dkgrey},

}


