diff options
Diffstat (limited to 'doc/common')
19 files changed, 2918 insertions, 0 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex new file mode 100644 index 0000000000..e790d20e00 --- /dev/null +++ b/doc/common/macros.tex @@ -0,0 +1,546 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% MACROS FOR THE REFERENCE MANUAL OF COQ % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% For commentaries (define \com as {} for the release manual) +%\newcommand{\com}[1]{{\it(* #1 *)}} +%\newcommand{\com}[1]{} + +%%OPTIONS for HACHA +%\renewcommand{\cuttingunit}{section} + + +%BEGIN LATEX +\newenvironment{centerframe}% +{\bgroup +\dimen0=\textwidth +\advance\dimen0 by -2\fboxrule +\advance\dimen0 by -2\fboxsep +\setbox0=\hbox\bgroup +\begin{minipage}{\dimen0}% +\begin{center}}% +{\end{center}% +\end{minipage}\egroup +\centerline{\fbox{\box0}}\egroup +} +%END LATEX +%HEVEA \newenvironment{centerframe}{\begin{center}}{\end{center}} + +%HEVEA \renewcommand{\vec}[1]{\mathbf{#1}} +%\renewcommand{\ominus}{-} % Hevea does a good job translating these commands +%\renewcommand{\oplus}{+} +%\renewcommand{\otimes}{\times} +%\newcommand{\land}{\wedge} +%\newcommand{\lor}{\vee} +%HEVEA \renewcommand{\k}[1]{#1} % \k{a} is supposed to produce a with a little stroke +%HEVEA \newcommand{\phantom}[1]{\qquad} + +%%%%%%%%%%%%%%%%%%%%%%% +% Formatting commands % +%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\ErrMsg}{\medskip \noindent {\bf Error message: }} +\newcommand{\ErrMsgx}{\medskip \noindent {\bf Error messages: }} +\newcommand{\variant}{\medskip \noindent {\bf Variant: }} +\newcommand{\variants}{\medskip \noindent {\bf Variants: }} +\newcommand{\SeeAlso}{\medskip \noindent {\bf See also: }} +\newcommand{\Rem}{\medskip \noindent {\bf Remark: }} +\newcommand{\Rems}{\medskip \noindent {\bf Remarks: }} +\newcommand{\Example}{\medskip \noindent {\bf Example: }} +\newcommand{\examples}{\medskip \noindent {\bf Examples: }} +\newcommand{\Warning}{\medskip \noindent {\bf Warning: }} +\newcommand{\Warns}{\medskip \noindent {\bf Warnings: }} +\newcounter{ex} +\newcommand{\firstexample}{\setcounter{ex}{1}} +\newcommand{\example}[1]{ +\medskip \noindent \textbf{Example \arabic{ex}: }\textit{#1} +\addtocounter{ex}{1}} + +\newenvironment{Variant}{\variant\begin{enumerate}}{\end{enumerate}} +\newenvironment{Variants}{\variants\begin{enumerate}}{\end{enumerate}} +\newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}} +\newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}} +\newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}} +\newenvironment{Examples}{\medskip\noindent{\bf Examples:} +\begin{enumerate}}{\end{enumerate}} + +%\newcommand{\bd}{\noindent\bf} +%\newcommand{\sbd}{\vspace{8pt}\noindent\bf} +%\newcommand{\sdoll}[1]{\begin{small}$ #1~ $\end{small}} +%\newcommand{\sdollnb}[1]{\begin{small}$ #1 $\end{small}} +\newcommand{\kw}[1]{\textsf{#1}} +%\newcommand{\spec}[1]{\{\,#1\,\}} + +% Building regular expressions +\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}} +\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}} +%\newcommand{\zeroonemany}[1]{$\{$#1$\}$*} +%\newcommand{\onemany}[1]{$\{$#1$\}$+} +\newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}} +\newcommand{\nelist}[2]{{#1} {\tt #2} \mbox{\dots} {\tt #2} {#1}} +\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2} \mbox{\dots} {\tt #2} {#1}{\sl ]}} +\newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\mbox{\dots}{\tt #2}#1} +\newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\mbox{\dots}{\tt #2}#1$]$} + +% Used for RefMan-gal +%\newcommand{\ml}[1]{\hbox{\tt{#1}}} +%\newcommand{\op}{\,|\,} + +%%%%%%%%%%%%%%%%%%%%%%%% +% Trademarks and so on % +%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\Coq}{\textsc{Coq}} +\newcommand{\gallina}{\textsc{Gallina}} +\newcommand{\Gallina}{\textsc{Gallina}} +\newcommand{\CoqIDE}{\textsc{CoqIDE}} +\newcommand{\ocaml}{\textsc{OCaml}} +\newcommand{\camlpppp}{\textsc{Camlp5}} +\newcommand{\emacs}{\textsc{GNU Emacs}} +\newcommand{\ProofGeneral}{\textsc{Proof General}} +\newcommand{\CIC}{\textsc{Cic}} +\newcommand{\iCIC}{\textsc{Cic}} +\newcommand{\FW}{\ensuremath{F_{\omega}}} +\newcommand{\Program}{\textsc{Program}} +\newcommand{\Russell}{\textsc{Russell}} +\newcommand{\PVS}{\textsc{PVS}} +%\newcommand{\bn}{{\sf BNF}} + +%%%%%%%%%%%%%%%%%%% +% Name of tactics % +%%%%%%%%%%%%%%%%%%% + +%\newcommand{\Natural}{\mbox{\tt Natural}} + +%%%%%%%%%%%%%%%%% +% \rm\sl series % +%%%%%%%%%%%%%%%%% + +\newcommand{\nterm}[1]{\textrm{\textsl{#1}}} + +\newcommand{\qstring}{\nterm{string}} + +%% New syntax specific entries +\newcommand{\annotation}{\nterm{annotation}} +\newcommand{\assums}{\nterm{assums}} % vernac +\newcommand{\simpleassums}{\nterm{simple\_assums}} % assumptions +\newcommand{\binder}{\nterm{binder}} +\newcommand{\binders}{\nterm{binders}} +\newcommand{\caseitems}{\nterm{match\_items}} +\newcommand{\caseitem}{\nterm{match\_item}} +\newcommand{\eqn}{\nterm{equation}} +\newcommand{\ifitem}{\nterm{dep\_ret\_type}} +\newcommand{\hyplocation}{\nterm{hyp\_location}} +\newcommand{\convclause}{\nterm{conversion\_clause}} +\newcommand{\occclause}{\nterm{occurrence\_clause}} +\newcommand{\occgoalset}{\nterm{goal\_occurrences}} +\newcommand{\atoccurrences}{\nterm{at\_occurrences}} +\newcommand{\occlist}{\nterm{occurrences}} +\newcommand{\params}{\nterm{params}} % vernac +\newcommand{\returntype}{\nterm{return\_type}} +\newcommand{\idparams}{\nterm{ident\_with\_params}} +\newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac +\newcommand{\termarg}{\nterm{arg}} +\newcommand{\hintdef}{\nterm{hint\_definition}} + +\newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}} +\newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}} +\newcommand{\typecstrtype}{\zeroone{{\tt :}~{\type}}} + +\newcommand{\Fwterm}{\nterm{Fwterm}} +\newcommand{\Index}{\nterm{index}} +\newcommand{\abbrev}{\nterm{abbreviation}} +\newcommand{\atomictac}{\nterm{atomic\_tactic}} +\newcommand{\bindinglist}{\nterm{bindings\_list}} +\newcommand{\cast}{\nterm{cast}} +\newcommand{\cofixpointbodies}{\nterm{cofix\_bodies}} +\newcommand{\cofixpointbody}{\nterm{cofix\_body}} +\newcommand{\commandtac}{\nterm{tactic\_invocation}} +\newcommand{\constructor}{\nterm{constructor}} +\newcommand{\convtactic}{\nterm{conv\_tactic}} +\newcommand{\assumptionkeyword}{\nterm{assumption\_keyword}} +\newcommand{\assumption}{\nterm{assumption}} +\newcommand{\definition}{\nterm{definition}} +\newcommand{\digit}{\nterm{digit}} +\newcommand{\exteqn}{\nterm{ext\_eqn}} +\newcommand{\field}{\nterm{field}} +\newcommand{\fielddef}{\nterm{field\_def}} +\newcommand{\firstletter}{\nterm{first\_letter}} +\newcommand{\fixpg}{\nterm{fix\_pgm}} +\newcommand{\fixpointbodies}{\nterm{fix\_bodies}} +\newcommand{\fixpointbody}{\nterm{fix\_body}} +\newcommand{\fixpoint}{\nterm{fixpoint}} +\newcommand{\flag}{\nterm{flag}} +\newcommand{\form}{\nterm{form}} +\newcommand{\entry}{\nterm{entry}} +\newcommand{\proditem}{\nterm{prod\_item}} +\newcommand{\taclevel}{\nterm{tactic\_level}} +\newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} +\newcommand{\scope}{\nterm{scope}} +\newcommand{\delimkey}{\nterm{key}} +\newcommand{\optscope}{\nterm{opt\_scope}} +\newcommand{\declnotation}{\nterm{decl\_notation}} +\newcommand{\symbolentry}{\nterm{symbol}} +\newcommand{\modifiers}{\nterm{modifiers}} +\newcommand{\binderinterp}{\nterm{binder\_interp}} +\newcommand{\localdef}{\nterm{local\_def}} +\newcommand{\localdecls}{\nterm{local\_decls}} +\newcommand{\ident}{\nterm{ident}} +\newcommand{\accessident}{\nterm{access\_ident}} +\newcommand{\possiblybracketedident}{\nterm{possibly\_bracketed\_ident}} +\newcommand{\inductivebody}{\nterm{ind\_body}} +\newcommand{\inductive}{\nterm{inductive}} +\newcommand{\naturalnumber}{\nterm{natural}} +\newcommand{\integer}{\nterm{integer}} +\newcommand{\multpattern}{\nterm{mult\_pattern}} +\newcommand{\mutualcoinductive}{\nterm{mutual\_coinductive}} +\newcommand{\mutualinductive}{\nterm{mutual\_inductive}} +\newcommand{\nestedpattern}{\nterm{nested\_pattern}} +\newcommand{\name}{\nterm{name}} +\newcommand{\num}{\nterm{num}} +\newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching +\newcommand{\orpattern}{\nterm{or\_pattern}} +\newcommand{\intropattern}{\nterm{intro\_pattern}} +\newcommand{\intropatternlist}{\nterm{intro\_pattern\_list}} +\newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}} +\newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}} +\newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes +\newcommand{\pat}{\nterm{pat}} +\newcommand{\pgs}{\nterm{pgms}} +\newcommand{\pg}{\nterm{pgm}} +\newcommand{\abullet}{\nterm{bullet}} +%BEGIN LATEX +\newcommand{\proof}{\nterm{proof}} +%END LATEX +%HEVEA \renewcommand{\proof}{\nterm{proof}} +\newcommand{\record}{\nterm{record}} +\newcommand{\recordkw}{\nterm{record\_keyword}} +\newcommand{\rewrule}{\nterm{rewriting\_rule}} +\newcommand{\sentence}{\nterm{sentence}} +\newcommand{\simplepattern}{\nterm{simple\_pattern}} +\newcommand{\sort}{\nterm{sort}} +\newcommand{\specif}{\nterm{specif}} +\newcommand{\assertion}{\nterm{assertion}} +\newcommand{\str}{\nterm{string}} +\newcommand{\subsequentletter}{\nterm{subsequent\_letter}} +\newcommand{\switch}{\nterm{switch}} +\newcommand{\messagetoken}{\nterm{message\_token}} +\newcommand{\tac}{\nterm{tactic}} +\newcommand{\terms}{\nterm{terms}} +\newcommand{\term}{\nterm{term}} +\newcommand{\module}{\nterm{module}} +\newcommand{\modexpr}{\nterm{module\_expression}} +\newcommand{\modtype}{\nterm{module\_type}} +\newcommand{\onemodbinding}{\nterm{module\_binding}} +\newcommand{\modbindings}{\nterm{module\_bindings}} +\newcommand{\qualid}{\nterm{qualid}} +\newcommand{\qualidorstring}{\nterm{qualid\_or\_string}} +\newcommand{\class}{\nterm{class}} +\newcommand{\dirpath}{\nterm{dirpath}} +\newcommand{\typedidents}{\nterm{typed\_idents}} +\newcommand{\type}{\nterm{type}} +\newcommand{\vref}{\nterm{ref}} +\newcommand{\zarithformula}{\nterm{zarith\_formula}} +\newcommand{\zarith}{\nterm{zarith}} +\newcommand{\ltac}{\mbox{${\mathcal{L}}_{tac}$}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% \mbox{\sf } series for roman text in maths formulas % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\alors}{\mbox{\textsf{then}}} +\newcommand{\alter}{\mbox{\textsf{alter}}} +\newcommand{\bool}{\mbox{\textsf{bool}}} +\newcommand{\conc}{\mbox{\textsf{conc}}} +\newcommand{\cons}{\mbox{\textsf{cons}}} +\newcommand{\consf}{\mbox{\textsf{consf}}} +\newcommand{\emptyf}{\mbox{\textsf{emptyf}}} +\newcommand{\EqSt}{\mbox{\textsf{EqSt}}} +\newcommand{\false}{\mbox{\textsf{false}}} +\newcommand{\filter}{\mbox{\textsf{filter}}} +\newcommand{\forest}{\mbox{\textsf{forest}}} +\newcommand{\from}{\mbox{\textsf{from}}} +\newcommand{\hd}{\mbox{\textsf{hd}}} +\newcommand{\haslength}{\mbox{\textsf{has\_length}}} +\newcommand{\length}{\mbox{\textsf{length}}} +\newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}} +\newcommand{\List}{\mbox{\textsf{list}}} +\newcommand{\ListA}{\mbox{\textsf{list}}~\ensuremath{A}} +\newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}} +\newcommand{\conshl}{\mbox{\textsf{cons\_hl}}} +\newcommand{\nat}{\mbox{\textsf{nat}}} +\newcommand{\nO}{\mbox{\textsf{O}}} +\newcommand{\nS}{\mbox{\textsf{S}}} +\newcommand{\node}{\mbox{\textsf{node}}} +\newcommand{\Nil}{\mbox{\textsf{nil}}} +\newcommand{\SProp}{\mbox{\textsf{SProp}}} +\newcommand{\Prop}{\mbox{\textsf{Prop}}} +\newcommand{\Set}{\mbox{\textsf{Set}}} +\newcommand{\si}{\mbox{\textsf{if}}} +\newcommand{\sinon}{\mbox{\textsf{else}}} +\newcommand{\Str}{\mbox{\textsf{Stream}}} +\newcommand{\tl}{\mbox{\textsf{tl}}} +\newcommand{\tree}{\mbox{\textsf{tree}}} +\newcommand{\true}{\mbox{\textsf{true}}} +\newcommand{\Type}{\mbox{\textsf{Type}}} +\newcommand{\unfold}{\mbox{\textsf{unfold}}} +\newcommand{\zeros}{\mbox{\textsf{zeros}}} +\newcommand{\even}{\mbox{\textsf{even}}} +\newcommand{\odd}{\mbox{\textsf{odd}}} +\newcommand{\evenO}{\mbox{\textsf{even\_O}}} +\newcommand{\evenS}{\mbox{\textsf{even\_S}}} +\newcommand{\oddS}{\mbox{\textsf{odd\_S}}} +\newcommand{\Prod}{\mbox{\textsf{prod}}} +\newcommand{\Pair}{\mbox{\textsf{pair}}} + +%%%%%%%%% +% Misc. % +%%%%%%%%% +\newcommand{\T}{\texttt{T}} +\newcommand{\U}{\texttt{U}} +\newcommand{\real}{\textsf{Real}} +\newcommand{\Data}{\textit{Data}} +\newcommand{\In} {{\textbf{in }}} +\newcommand{\AND} {{\textbf{and}}} +\newcommand{\If}{{\textbf{if }}} +\newcommand{\Else}{{\textbf{else }}} +\newcommand{\Then} {{\textbf{then }}} +%\newcommand{\Let}{{\textbf{let }}} % looks like this is never used +\newcommand{\Where}{{\textbf{where rec }}} +\newcommand{\Function}{{\textbf{function }}} +\newcommand{\Rec}{{\textbf{rec }}} +%\newcommand{\cn}{\centering} +\newcommand{\nth}{\mbox{$^{\mbox{\scriptsize th}}$}} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% Math commands and symbols % +%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\la}{\leftarrow} +\newcommand{\ra}{\rightarrow} +\newcommand{\Ra}{\Rightarrow} +\newcommand{\rt}{\Rightarrow} +\newcommand{\lla}{\longleftarrow} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Llra}{\Longleftrightarrow} +\newcommand{\mt}{\mapsto} +\newcommand{\ov}{\overrightarrow} +\newcommand{\wh}{\widehat} +\newcommand{\up}{\uparrow} +\newcommand{\dw}{\downarrow} +\newcommand{\nr}{\nearrow} +\newcommand{\se}{\searrow} +\newcommand{\sw}{\swarrow} +\newcommand{\nw}{\nwarrow} +\newcommand{\mto}{.\;} + +\newcommand{\vm}[1]{\vspace{#1em}} +\newcommand{\vx}[1]{\vspace{#1ex}} +\newcommand{\hm}[1]{\hspace{#1em}} +\newcommand{\hx}[1]{\hspace{#1ex}} +\newcommand{\sm}{\mbox{ }} +\newcommand{\mx}{\mbox} + +%\newcommand{\nq}{\neq} +%\newcommand{\eq}{\equiv} +\newcommand{\fa}{\forall} +%\newcommand{\ex}{\exists} +\newcommand{\impl}{\rightarrow} +%\newcommand{\Or}{\vee} +%\newcommand{\And}{\wedge} +\newcommand{\ms}{\models} +\newcommand{\bw}{\bigwedge} +\newcommand{\ts}{\times} +\newcommand{\cc}{\circ} +%\newcommand{\es}{\emptyset} +%\newcommand{\bs}{\backslash} +\newcommand{\vd}{\vdash} +%\newcommand{\lan}{{\langle }} +%\newcommand{\ran}{{\rangle }} + +%\newcommand{\al}{\alpha} +\newcommand{\bt}{\beta} +%\newcommand{\io}{\iota} +\newcommand{\lb}{\lambda} +%\newcommand{\sg}{\sigma} +%\newcommand{\sa}{\Sigma} +%\newcommand{\om}{\Omega} +%\newcommand{\tu}{\tau} + +%%%%%%%%%%%%%%%%%%%%%%%%% +% Custom maths commands % +%%%%%%%%%%%%%%%%%%%%%%%%% + +\newcommand{\sumbool}[2]{\{#1\}+\{#2\}} +\newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3} +\newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2} +\newcommand{\WF}[2]{\ensuremath{{\mathcal{W\!F}}(#1)[#2]}} +\newcommand{\WFTWOLINES}[2]{\ensuremath{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} + +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\WFT}[2]{\ensuremath{#1[] \vdash {\mathcal{W\!F}}(#2)}} +\newcommand{\WS}[3]{\ensuremath{#1[] \vdash #2 <: #3}} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} + +\newcommand{\WTRED}[5]{\mbox{$#1[#2] \vdash #3 #4 #5$}} +\newcommand{\WTERED}[4]{\mbox{$E[#1] \vdash #2 #3 #4$}} +\newcommand{\WTELECONV}[3]{\WTERED{#1}{#2}{\leconvert}{#3}} +\newcommand{\WTEGRED}[3]{\WTERED{\Gamma}{#1}{#2}{#3}} +\newcommand{\WTECONV}[3]{\WTERED{#1}{#2}{\convert}{#3}} +\newcommand{\WTEGCONV}[2]{\WTERED{\Gamma}{#1}{\convert}{#2}} +\newcommand{\WTEGLECONV}[2]{\WTERED{\Gamma}{#1}{\leconvert}{#2}} + +\newcommand{\lab}[1]{\mathit{labels}(#1)} +\newcommand{\dom}[1]{\mathit{dom}(#1)} + +\newcommand{\CI}[2]{\mbox{$\{#1\}^{#2}$}} +\newcommand{\CIP}[3]{\mbox{$\{#1\}_{#2}^{#3}$}} +\newcommand{\CIPV}[1]{\CIP{#1}{I_1.. I_k}{P_1.. P_k}} +\newcommand{\CIPI}[1]{\CIP{#1}{I}{P}} +\newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}} +%BEGIN LATEX +\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(\begin{array}[t]{@{}l}#2:=#3 + \,)\end{array}$}} +\newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4 + \,)\end{array}$}} +%END LATEX +%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}} +%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}} + +\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4 + \,)\end{array}$}} +\newcommand{\Indpstr}[6]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4 + \,)/{#6}\end{array}$}} +\newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}} +\newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}} +\newcommand{\Match}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Match}}~#2~{\mbox{\tt with}}~#3~{\mbox{\tt end}}$}} +\newcommand{\Case}[3]{\mbox{$\kw{case}(#2,#1,#3)$}} +\newcommand{\match}[3]{\mbox{$\kw{match}~ #2 ~\kw{with}~ #3 ~\kw{end}$}} +\newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}} +\newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}} +\newcommand{\With}[2]{\mbox{\tt ~with~}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}} +\newcommand{\Sort}{\mbox{$\mathcal{S}$}} +\newcommand{\convert}{=_{\beta\delta\iota\zeta\eta}} +\newcommand{\leconvert}{\leq_{\beta\delta\iota\zeta\eta}} +\newcommand{\NN}{\mathbb{N}} +\newcommand{\inference}[1]{$${#1}$$} + +\newcommand{\compat}[2]{\mbox{$[#1|#2]$}} +\newcommand{\tristackrel}[3]{\mathrel{\mathop{#2}\limits_{#3}^{#1}}} + +\newcommand{\Impl}{{\it Impl}} +\newcommand{\elem}{{\it e}} +\newcommand{\Mod}[3]{{\sf Mod}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModS}[2]{{\sf Mod}({#1}:{#2})} +\newcommand{\ModType}[2]{{\sf ModType}({#1}:={#2})} +\newcommand{\ModA}[2]{{\sf ModA}({#1}=={#2})} +\newcommand{\functor}[3]{\ensuremath{{\sf Functor}(#1:#2)\;#3}} +\newcommand{\funsig}[3]{\ensuremath{{\sf Funsig}(#1:#2)\;#3}} +\newcommand{\sig}[1]{\ensuremath{{\sf Sig}~#1~{\sf End}}} +\newcommand{\struct}[1]{\ensuremath{{\sf Struct}~#1~{\sf End}}} +\newcommand{\structe}[1]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2};\ldots + ;\elem_n~{\sf End}}} +\newcommand{\structes}[2]{\ensuremath{ + {\sf Struct}~\elem_1;\ldots;\elem_i;#1;\elem_{i+2}\{#2\} + ;\ldots;\elem_n\{#2\}~{\sf End}}} +\newcommand{\with}[3]{\ensuremath{#1~{\sf with}~#2 := #3}} + +\newcommand{\Spec}{{\it Spec}} +\newcommand{\ModSEq}[3]{{\sf Mod}({#1}:{#2}:={#3})} + + +%\newbox\tempa +%\newbox\tempb +%\newdimen\tempc +%\newcommand{\mud}[1]{\hfil $\displaystyle{\mathstrut #1}$\hfil} +%\newcommand{\rig}[1]{\hfil $\displaystyle{#1}$} +% \newcommand{\irulehelp}[3]{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}% +% \setbox\tempb=\vbox{\halign{##\cr +% \mud{#1}\cr +% \noalign{\vskip\the\lineskip} +% \noalign{\hrule height 0pt} +% \rig{\vbox to 0pt{\vss\hbox to 0pt{${\; #3}$\hss}\vss}}\cr +% \noalign{\hrule} +% \noalign{\vskip\the\lineskip} +% \mud{\copy\tempa}\cr}} +% \tempc=\wd\tempb +% \advance\tempc by \wd\tempa +% \divide\tempc by 2 } +% \newcommand{\irule}[3]{{\irulehelp{#1}{#2}{#3} +% \hbox to \wd\tempa{\hss \box\tempb \hss}}} + +\newcommand{\sverb}[1]{{\tt #1}} +\newcommand{\mover}[2]{{#1\over #2}} +\newcommand{\jd}[2]{#1 \vdash #2} +\newcommand{\mathline}[1]{\[#1\]} +\newcommand{\zrule}[2]{#2: #1} +\newcommand{\orule}[3]{#3: {\mover{#1}{#2}}} +\newcommand{\trule}[4]{#4: \mover{#1 \qquad #2} {#3}} +\newcommand{\thrule}[5]{#5: {\mover{#1 \qquad #2 \qquad #3}{#4}}} + + + +% placement of figures + +%BEGIN LATEX +\renewcommand{\topfraction}{.99} +\renewcommand{\bottomfraction}{.99} +\renewcommand{\textfraction}{.01} +\renewcommand{\floatpagefraction}{.9} +%END LATEX + +% Macros Bruno pour description de la syntaxe + +\def\bfbar{\ensuremath{|\hskip -0.22em{}|\hskip -0.24em{}|}} +\def\TERMbar{\bfbar} +\def\TERMbarbar{\bfbar\bfbar} + + +%% Macros pour les grammaires +\def\GR#1{\text{\large(}#1\text{\large)}} +\def\NT#1{\langle\textit{#1}\rangle} +\def\NTL#1#2{\langle\textit{#1}\rangle_{#2}} +\def\TERM#1{{\bf\textrm{\bf #1}}} +%\def\TERM#1{{\bf\textsf{#1}}} +\def\KWD#1{\TERM{#1}} +\def\ETERM#1{\TERM{#1}} +\def\CHAR#1{\TERM{#1}} + +\def\STAR#1{#1*} +\def\STARGR#1{\GR{#1}*} +\def\PLUS#1{#1+} +\def\PLUSGR#1{\GR{#1}+} +\def\OPT#1{#1?} +\def\OPTGR#1{\GR{#1}?} +%% Tableaux de definition de non-terminaux +\newenvironment{cadre} + {\begin{array}{|c|}\hline\\} + {\\\\\hline\end{array}} +\newenvironment{rulebox} + {$$\begin{cadre}\begin{array}{r@{~}c@{~}l@{}l@{}r}} + {\end{array}\end{cadre}$$} +\def\DEFNT#1{\NT{#1} & ::= &} +\def\EXTNT#1{\NT{#1} & ::= & ... \\&|&} +\def\RNAME#1{(\textsc{#1})} +\def\SEPDEF{\\\\} +\def\nlsep{\\&|&} +\def\nlcont{\\&&} +\newenvironment{rules} + {\begin{center}\begin{rulebox}} + {\end{rulebox}\end{center}} + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html new file mode 100644 index 0000000000..5d151381ff --- /dev/null +++ b/doc/common/styles/html/coqremote/cover.html @@ -0,0 +1,109 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> + +<head> + +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/system/system.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/user/user.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/style.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/coqdoc.css" /> + +<title>Reference Manual | The Coq Proof Assistant</title> + +</head> + +<body> + +<div id="container"> + +<div id="headertop"> +<div id="nav"> + <ul class="links-menu"> + <li><a href="/" class="active">Home</a></li> + <li><a href="/about-coq" title="More about coq">About Coq</a></li> + <li><a href="/download">Get Coq</a></li> + <li><a href="/documentation">Documentation</a></li> + <li><a href="/community">Community</a></li> + </ul> +</div> +</div> + +<div id="header"> +<div id="logoWrapper"> + <div id="logo"><a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a> + </div> + <div id="siteName"><a href="/" title="Home">The Coq Proof Assistant</a> + </div> +</div> +</div> + +<div id="content"> + +<br /> +<h1 style="text-align:center; font-weight:bold; font-size: 300%; line-height: 2ex">Reference Manual</h1> + +<h2 style="text-align:center; font-size: 120%">Version COQVERSION</h2> +<br /> + +<h2 style="text-align:center; font-size: 150%">The Coq Development Team</h2> +<br /><br /><br /> + +<p style="text-indent:0pt">Copyright © INRIA 1999-2017</p> + +<p style="text-indent:0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> + +</div> +</div> +</div> + +<div id="sidebarWrapper"> +<div id="sidebar"> + +<div class="block"> +<h2 class="title">Navigation</h2> +<div class="content"> + +<ul class="menu"> + +<li class="leaf"><a href="index.html">Cover</a></li> + +<li class="leaf"><a href="toc.html">Table of contents</a></li> +<li class="leaf">Index + <ul class="menu"> + <li><a href="general-index.html">General</a></li> + <li><a href="command-index.html">Commands</a></li> + <li><a href="option-index.html">Options</a></li> + <li><a href="tactic-index.html">Tactics</a></li> + <li><a href="error-index.html">Errors</a></li> + </ul> + +</li> + +</ul> + +</div> +</div> + +</div> +</div> + + +<div id="footer"> +<div id="nav-footer"> + <ul class="links-menu-footer"> + <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li> + <li><a href="http://validator.w3.org/">xhtml valid</a></li> + <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li> + </ul> + +</div> + +</div> + +</body> + +</html> diff --git a/doc/common/styles/html/coqremote/footer.html b/doc/common/styles/html/coqremote/footer.html new file mode 100644 index 0000000000..23dfccb62c --- /dev/null +++ b/doc/common/styles/html/coqremote/footer.html @@ -0,0 +1,34 @@ + <div id="sidebarWrapper"> + <div id="sidebar"> + <div class="block"> + <h2 class="title">Navigation</h2> + <div class="content"> + <ul class="menu"> + <li class="leaf">Standard Library + <ul class="menu"> + <li><a href="index.html">Table of contents</a></li> + <li><a href="genindex.html">Index</a></li> + </ul> + </li> + </ul> + </div> + </div> + </div> + </div> + + </div> + + <div id="footer"> + <div id="nav-footer"> + <ul class="links-menu-footer"> + <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li> + <li><a href="http://validator.w3.org/">xhtml valid</a></li> + <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li> + </ul> + </div> + </div> + +</div> + +</body> +</html> diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html new file mode 100644 index 0000000000..2f7ba14753 --- /dev/null +++ b/doc/common/styles/html/coqremote/header.html @@ -0,0 +1,43 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> + +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css" /> + +<title>Standard Library | The Coq Proof Assistant</title> + +</head> + +<body> + +<div id="container"> + <div id="headertop"> + <div id="nav"> + <ul class="links-menu"> + <li><a href="//coq.inria.fr/" class="active">Home</a></li> + <li><a href="//coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> + <li><a href="//coq.inria.fr/download">Get Coq</a></li> + <li><a href="//coq.inria.fr/documentation">Documentation</a></li> + <li><a href="//coq.inria.fr/community">Community</a></li> + </ul> + </div> + </div> + + <div id="header"> + <div id="logoWrapper"> + <div id="logo"><a href="//coq.inria.fr/" title="Home"><img src="//coq.inria.fr/files/barron_logo.png" alt="Home" /></a> + </div> + <div id="siteName"><a href="//coq.inria.fr/" title="Home">The Coq Proof Assistant</a> + </div> + </div> + </div> + + <div id="content"> + diff --git a/doc/common/styles/html/coqremote/hevea.css b/doc/common/styles/html/coqremote/hevea.css new file mode 100644 index 0000000000..5f4edef6f1 --- /dev/null +++ b/doc/common/styles/html/coqremote/hevea.css @@ -0,0 +1,36 @@ + +.li-itemize{margin:1ex 0ex;} +.li-enumerate{margin:1ex 0ex;} +.dd-description{margin:0ex 0ex 1ex 4ex;} +.dt-description{margin:0ex;} +.toc{list-style:none;} +.thefootnotes{text-align:left;margin:0ex;} +.dt-thefootnotes{margin:0em;} +.dd-thefootnotes{margin:0em 0em 0em 2em;} +.footnoterule{margin:1em auto 1em 0px;width:50%;} +.caption{padding-left:2ex; padding-right:2ex; margin-left:auto; margin-right:auto} +.title{margin:2ex auto;text-align:center} +.center{text-align:center;margin-left:auto;margin-right:auto;} +.flushleft{text-align:left;margin-left:0ex;margin-right:auto;} +.flushright{text-align:right;margin-left:auto;margin-right:0ex;} +DIV TABLE{margin-left:inherit;margin-right:inherit;} +PRE{text-align:left;margin-left:0ex;margin-right:auto;} +BLOCKQUOTE{margin-left:4ex;margin-right:4ex;text-align:left;} +TD P{margin:0px;} +.boxed{border:1px solid black} +.textboxed{border:1px solid black} +.vbar{border:none;width:2px;background-color:black;} +.hbar{border:none;height:2px;width:100%;background-color:black;} +.hfill{border:none;height:1px;width:200%;background-color:black;} +.vdisplay{border-collapse:separate;border-spacing:2px;width:auto; empty-cells:show; border:2px solid red;} +.vdcell{white-space:nowrap;padding:0px;width:auto; border:2px solid green;} +.display{border-collapse:separate;border-spacing:2px;width:auto; border:none;} +.dcell{white-space:nowrap;padding:0px;width:auto; border:none;} +.dcenter{margin:0ex auto;} +.vdcenter{border:solid #FF8000 2px; margin:0ex auto;} +.minipage{text-align:left; margin-left:0em; margin-right:auto;} +.marginpar{border:solid thin black; width:20%; text-align:left;} +.marginparleft{float:left; margin-left:0ex; margin-right:1ex;} +.marginparright{float:right; margin-left:1ex; margin-right:0ex;} +.theorem{text-align:left;margin:1ex auto 1ex 0ex;} +.part{margin:2ex auto;text-align:center} diff --git a/doc/common/styles/html/coqremote/modules/node/node.css b/doc/common/styles/html/coqremote/modules/node/node.css new file mode 100644 index 0000000000..60d01308e9 --- /dev/null +++ b/doc/common/styles/html/coqremote/modules/node/node.css @@ -0,0 +1,43 @@ + +.node-unpublished { + background-color: #fff4f4; +} +.preview .node { + background-color: #ffffea; +} +#node-admin-filter ul { + list-style-type: none; + padding: 0; + margin: 0; + width: 100%; +} +#node-admin-buttons { + float: left; /* LTR */ + margin-left: 0.5em; /* LTR */ + clear: right; /* LTR */ +} +td.revision-current { + background: #ffc; +} +.node-form .form-text { + display: block; + width: 95%; +} +.node-form .container-inline .form-text { + display: inline; + width: auto; +} +.node-form .standard { + clear: both; +} +.node-form textarea { + display: block; + width: 95%; +} +.node-form .attachments fieldset { + float: none; + display: block; +} +.terms-inline { + display: inline; +} diff --git a/doc/common/styles/html/coqremote/modules/system/defaults.css b/doc/common/styles/html/coqremote/modules/system/defaults.css new file mode 100644 index 0000000000..eb983b7f81 --- /dev/null +++ b/doc/common/styles/html/coqremote/modules/system/defaults.css @@ -0,0 +1,52 @@ + +/* +** HTML elements +*/ +fieldset { + margin-bottom: 1em; + padding: .5em; +} +form { + margin: 0; + padding: 0; +} +hr { + height: 1px; + border: 1px solid gray; +} +img { + border: 0; +} +table { + border-collapse: collapse; +} +th { + text-align: left; /* LTR */ + padding-right: 1em; /* LTR */ + border-bottom: 3px solid #ccc; +} + +/* +** Markup free clearing +** Details: http://www.positioniseverything.net/easyclearing.html +*/ +.clear-block:after { + content: "."; + display: block; + height: 0; + clear: both; + visibility: hidden; +} + +.clear-block { + display: inline-block; +} + +/* Hides from IE-mac \*/ +* html .clear-block { + height: 1%; +} +.clear-block { + display: block; +} +/* End hide from IE-mac */ diff --git a/doc/common/styles/html/coqremote/modules/system/system.css b/doc/common/styles/html/coqremote/modules/system/system.css new file mode 100644 index 0000000000..9371bb479e --- /dev/null +++ b/doc/common/styles/html/coqremote/modules/system/system.css @@ -0,0 +1,543 @@ + +/* +** HTML elements +*/ +body.drag { + cursor: move; +} +th.active img { + display: inline; +} +tr.even, tr.odd { + background-color: #eee; + border-bottom: 1px solid #ccc; + padding: 0.1em 0.6em; +} +tr.drag { + background-color: #fffff0; +} +tr.drag-previous { + background-color: #ffd; +} +td.active { + background-color: #ddd; +} +td.checkbox, th.checkbox { + text-align: center; +} +tbody { + border-top: 1px solid #ccc; +} +tbody th { + border-bottom: 1px solid #ccc; +} +thead th { + text-align: left; /* LTR */ + padding-right: 1em; /* LTR */ + border-bottom: 3px solid #ccc; +} + +/* +** Other common styles +*/ +.breadcrumb { + padding-bottom: .5em +} +div.indentation { + width: 20px; + height: 1.7em; + margin: -0.4em 0.2em -0.4em -0.4em; /* LTR */ + padding: 0.42em 0 0.42em 0.6em; /* LTR */ + float: left; /* LTR */ +} +div.tree-child { + background: url(../../misc/tree.png) no-repeat 11px center; /* LTR */ +} +div.tree-child-last { + background: url(../../misc/tree-bottom.png) no-repeat 11px center; /* LTR */ +} +div.tree-child-horizontal { + background: url(../../misc/tree.png) no-repeat -11px center; +} +.error { + color: #e55; +} +div.error { + border: 1px solid #d77; +} +div.error, tr.error { + background: #fcc; + color: #200; + padding: 2px; +} +.warning { + color: #e09010; +} +div.warning { + border: 1px solid #f0c020; +} +div.warning, tr.warning { + background: #ffd; + color: #220; + padding: 2px; +} +.ok { + color: #008000; +} +div.ok { + border: 1px solid #00aa00; +} +div.ok, tr.ok { + background: #dfd; + color: #020; + padding: 2px; +} +.item-list .icon { + color: #555; + float: right; /* LTR */ + padding-left: 0.25em; /* LTR */ + clear: right; /* LTR */ +} +.item-list .title { + font-weight: bold; +} +.item-list ul { + margin: 0 0 0.75em 0; + padding: 0; +} +.item-list ul li { + margin: 0 0 0.25em 1.5em; /* LTR */ + padding: 0; + list-style: disc; +} +ol.task-list li.active { + font-weight: bold; +} +.form-item { + margin-top: 1em; + margin-bottom: 1em; +} +tr.odd .form-item, tr.even .form-item { + margin-top: 0; + margin-bottom: 0; + white-space: nowrap; +} +tr.merge-down, tr.merge-down td, tr.merge-down th { + border-bottom-width: 0 !important; +} +tr.merge-up, tr.merge-up td, tr.merge-up th { + border-top-width: 0 !important; +} +.form-item input.error, .form-item textarea.error, .form-item select.error { + border: 2px solid red; +} +.form-item .description { + font-size: 0.85em; +} +.form-item label { + display: block; + font-weight: bold; +} +.form-item label.option { + display: inline; + font-weight: normal; +} +.form-checkboxes, .form-radios { + margin: 1em 0; +} +.form-checkboxes .form-item, .form-radios .form-item { + margin-top: 0.4em; + margin-bottom: 0.4em; +} +.marker, .form-required { + color: #f00; +} +.more-link { + text-align: right; /* LTR */ +} +.more-help-link { + font-size: 0.85em; + text-align: right; /* LTR */ +} +.nowrap { + white-space: nowrap; +} +.item-list .pager { + clear: both; + text-align: center; +} +.item-list .pager li { + background-image:none; + display:inline; + list-style-type:none; + padding: 0.5em; +} +.pager-current { + font-weight:bold; +} +.tips { + margin-top: 0; + margin-bottom: 0; + padding-top: 0; + padding-bottom: 0; + font-size: 0.9em; +} +dl.multiselect dd.b, dl.multiselect dd.b .form-item, dl.multiselect dd.b select { + font-family: inherit; + font-size: inherit; + width: 14em; +} +dl.multiselect dd.a, dl.multiselect dd.a .form-item { + width: 10em; +} +dl.multiselect dt, dl.multiselect dd { + float: left; /* LTR */ + line-height: 1.75em; + padding: 0; + margin: 0 1em 0 0; /* LTR */ +} +dl.multiselect .form-item { + height: 1.75em; + margin: 0; +} + +/* +** Inline items (need to override above) +*/ +.container-inline div, .container-inline label { + display: inline; +} + +/* +** Tab navigation +*/ +ul.primary { + border-collapse: collapse; + padding: 0 0 0 1em; /* LTR */ + white-space: nowrap; + list-style: none; + margin: 5px; + height: auto; + line-height: normal; + border-bottom: 1px solid #bbb; +} +ul.primary li { + display: inline; +} +ul.primary li a { + background-color: #ddd; + border-color: #bbb; + border-width: 1px; + border-style: solid solid none solid; + height: auto; + margin-right: 0.5em; /* LTR */ + padding: 0 1em; + text-decoration: none; +} +ul.primary li.active a { + background-color: #fff; + border: 1px solid #bbb; + border-bottom: #fff 1px solid; +} +ul.primary li a:hover { + background-color: #eee; + border-color: #ccc; + border-bottom-color: #eee; +} +ul.secondary { + border-bottom: 1px solid #bbb; + padding: 0.5em 1em; + margin: 5px; +} +ul.secondary li { + display: inline; + padding: 0 1em; + border-right: 1px solid #ccc; /* LTR */ +} +ul.secondary a { + padding: 0; + text-decoration: none; +} +ul.secondary a.active { + border-bottom: 4px solid #999; +} + +/* +** Autocomplete styles +*/ +/* Suggestion list */ +#autocomplete { + position: absolute; + border: 1px solid; + overflow: hidden; + z-index: 100; +} +#autocomplete ul { + margin: 0; + padding: 0; + list-style: none; +} +#autocomplete li { + background: #fff; + color: #000; + white-space: pre; + cursor: default; +} +#autocomplete li.selected { + background: #0072b9; + color: #fff; +} +/* Animated throbber */ +html.js input.form-autocomplete { + background-image: url(../../misc/throbber.gif); + background-repeat: no-repeat; + background-position: 100% 2px; /* LTR */ +} +html.js input.throbbing { + background-position: 100% -18px; /* LTR */ +} + +/* +** Collapsing fieldsets +*/ +html.js fieldset.collapsed { + border-bottom-width: 0; + border-left-width: 0; + border-right-width: 0; + margin-bottom: 0; + height: 1em; +} +html.js fieldset.collapsed * { + display: none; +} +html.js fieldset.collapsed legend { + display: block; +} +html.js fieldset.collapsible legend a { + padding-left: 15px; /* LTR */ + background: url(../../misc/menu-expanded.png) 5px 75% no-repeat; /* LTR */ +} +html.js fieldset.collapsed legend a { + background-image: url(../../misc/menu-collapsed.png); /* LTR */ + background-position: 5px 50%; /* LTR */ +} +/* Note: IE-only fix due to '* html' (breaks Konqueror otherwise). */ +* html.js fieldset.collapsed legend, +* html.js fieldset.collapsed legend *, +* html.js fieldset.collapsed table * { + display: inline; +} +/* For Safari 2 to prevent collapsible fieldsets containing tables from dissapearing due to tableheader.js. */ +html.js fieldset.collapsible { + position: relative; +} +html.js fieldset.collapsible legend a { + display: block; +} +/* Avoid jumping around due to margins collapsing into collapsible fieldset border */ +html.js fieldset.collapsible .fieldset-wrapper { + overflow: auto; +} + +/* +** Resizable text areas +*/ +.resizable-textarea { + width: 95%; +} +.resizable-textarea .grippie { + height: 9px; + overflow: hidden; + background: #eee url(../../misc/grippie.png) no-repeat center 2px; + border: 1px solid #ddd; + border-top-width: 0; + cursor: s-resize; +} +html.js .resizable-textarea textarea { + margin-bottom: 0; + width: 100%; + display: block; +} + +/* +** Table drag and drop. +*/ +.draggable a.tabledrag-handle { + cursor: move; + float: left; /* LTR */ + height: 1.7em; + margin: -0.4em 0 -0.4em -0.5em; /* LTR */ + padding: 0.42em 1.5em 0.42em 0.5em; /* LTR */ + text-decoration: none; +} +a.tabledrag-handle:hover { + text-decoration: none; +} +a.tabledrag-handle .handle { + margin-top: 4px; + height: 13px; + width: 13px; + background: url(../../misc/draggable.png) no-repeat 0 0; +} +a.tabledrag-handle-hover .handle { + background-position: 0 -20px; +} + +/* +** Teaser splitter +*/ +.joined + .grippie { + height: 5px; + background-position: center 1px; + margin-bottom: -2px; +} +/* Keeps inner content contained in Opera 9. */ +.teaser-checkbox { + padding-top: 1px; +} +div.teaser-button-wrapper { + float: right; /* LTR */ + padding-right: 5%; /* LTR */ + margin: 0; +} +.teaser-checkbox div.form-item { + float: right; /* LTR */ + margin: 0 5% 0 0; /* LTR */ + padding: 0; +} +textarea.teaser { + display: none; +} +html.js .no-js { + display: none; +} + +/* +** Progressbar styles +*/ +.progress { + font-weight: bold; +} +.progress .bar { + background: #fff url(../../misc/progress.gif); + border: 1px solid #00375a; + height: 1.5em; + margin: 0 0.2em; +} +.progress .filled { + background: #0072b9; + height: 1em; + border-bottom: 0.5em solid #004a73; + width: 0%; +} +.progress .percentage { + float: right; /* LTR */ +} +.progress-disabled { + float: left; /* LTR */ +} +.ahah-progress { + float: left; /* LTR */ +} +.ahah-progress .throbber { + width: 15px; + height: 15px; + margin: 2px; + background: transparent url(../../misc/throbber.gif) no-repeat 0px -18px; + float: left; /* LTR */ +} +tr .ahah-progress .throbber { + margin: 0 2px; +} +.ahah-progress-bar { + width: 16em; +} + +/* +** Formatting for welcome page +*/ +#first-time strong { + display: block; + padding: 1.5em 0 .5em; +} + +/* +** To be used with tableselect.js +*/ +tr.selected td { + background: #ffc; +} + +/* +** Floating header for tableheader.js +*/ +table.sticky-header { + margin-top: 0; + background: #fff; +} + +/* +** Installation clean URLs +*/ +#clean-url.install { + display: none; +} + +/* +** For anything you want to hide on page load when JS is enabled, so +** that you can use the JS to control visibility and avoid flicker. +*/ +html.js .js-hide { + display: none; +} + +/* +** Styles for the system modules page (admin/build/modules) +*/ +#system-modules div.incompatible { + font-weight: bold; +} + +/* +** Styles for the system themes page (admin/build/themes) +*/ +#system-themes-form div.incompatible { + font-weight: bold; +} + +/* +** Password strength indicator +*/ +span.password-strength { + visibility: hidden; +} +input.password-field { + margin-right: 10px; /* LTR */ +} +div.password-description { + padding: 0 2px; + margin: 4px 0 0 0; + font-size: 0.85em; + max-width: 500px; +} +div.password-description ul { + margin-bottom: 0; +} +.password-parent { + margin: 0 0 0 0; +} +/* +** Password confirmation checker +*/ +input.password-confirm { + margin-right: 10px; /* LTR */ +} +.confirm-parent { + margin: 5px 0 0 0; +} +span.password-confirm { + visibility: hidden; +} +span.password-confirm span { + font-weight: normal; +} diff --git a/doc/common/styles/html/coqremote/modules/user/user.css b/doc/common/styles/html/coqremote/modules/user/user.css new file mode 100644 index 0000000000..7b2163e3d3 --- /dev/null +++ b/doc/common/styles/html/coqremote/modules/user/user.css @@ -0,0 +1,58 @@ + +#permissions td.module { + font-weight: bold; +} +#permissions td.permission { + padding-left: 1.5em; /* LTR */ +} +#access-rules .access-type, #access-rules .rule-type { + margin-right: 1em; /* LTR */ + float: left; /* LTR */ +} +#access-rules .access-type .form-item, #access-rules .rule-type .form-item { + margin-top: 0; +} +#access-rules .mask { + clear: both; +} +#user-login-form { + text-align: center; +} +#user-admin-filter ul { + list-style-type: none; + padding: 0; + margin: 0; + width: 100%; +} +#user-admin-buttons { + float: left; /* LTR */ + margin-left: 0.5em; /* LTR */ + clear: right; /* LTR */ +} +#user-admin-settings fieldset .description { + font-size: 0.85em; + padding-bottom: .5em; +} + +/* Generated by user.module but used by profile.module: */ +.profile { + clear: both; + margin: 1em 0; +} +.profile .picture { + float: right; /* LTR */ + margin: 0 1em 1em 0; /* LTR */ +} +.profile h3 { + border-bottom: 1px solid #ccc; +} +.profile dl { + margin: 0 0 1.5em 0; +} +.profile dt { + margin: 0 0 0.2em 0; + font-weight: bold; +} +.profile dd { + margin: 0 0 1em 0; +} diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css new file mode 100644 index 0000000000..d23ea8f362 --- /dev/null +++ b/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css @@ -0,0 +1,329 @@ +body { padding: 0px 0px; + margin: 0px 0px; + background-color: white } + +#page { display: block; + padding: 0px; + margin: 0px; + padding-bottom: 10px; } + +#header { display: block; + position: relative; + padding: 0; + margin: 0; + vertical-align: middle; + border-bottom-style: solid; + border-width: thin } + +#header h1 { padding: 0; + margin: 0;} + + +/* Contents */ + +#main{ display: block; + padding: 10px; + font-family: sans-serif; + font-size: 100%; + line-height: 100% } + +#main h1 { line-height: 95% } /* allow for multi-line headers */ + +#main a.idref:visited {color : #416DFF; text-decoration : none; } +#main a.idref:link {color : #416DFF; text-decoration : none; } +#main a.idref:hover {text-decoration : none; } +#main a.idref:active {text-decoration : none; } + +#main a.modref:visited {color : #416DFF; text-decoration : none; } +#main a.modref:link {color : #416DFF; text-decoration : none; } +#main a.modref:hover {text-decoration : none; } +#main a.modref:active {text-decoration : none; } + +#main .keyword { color : #cf1d1d } +#main { color: black } + +.section { background-color: rgb(60%,60%,100%); + padding-top: 13px; + padding-bottom: 13px; + padding-left: 3px; + margin-top: 5px; + margin-bottom: 5px; + font-size : 175% } + +h2.section { background-color: rgb(80%,80%,100%); + padding-left: 3px; + padding-top: 12px; + padding-bottom: 10px; + font-size : 130% } + +h3.section { background-color: rgb(90%,90%,100%); + padding-left: 3px; + padding-top: 7px; + padding-bottom: 7px; + font-size : 115% } + +h4.section { +/* + background-color: rgb(80%,80%,80%); + max-width: 20em; + padding-left: 5px; + padding-top: 5px; + padding-bottom: 5px; +*/ + background-color: white; + padding-left: 0px; + padding-top: 0px; + padding-bottom: 0px; + font-size : 100%; + font-weight : bold; + text-decoration : underline; + } + +#main .doc { margin: 0px; + font-family: sans-serif; + font-size: 100%; + line-height: 125%; + max-width: 40em; + color: black; + padding: 10px; + background-color: #90bdff} + +.inlinecode { + display: inline; +/* font-size: 125%; */ + color: #666666; + font-family: monospace } + +.doc .inlinecode { + display: inline; + font-size: 120%; + color: rgb(30%,30%,70%); + font-family: monospace } + +.doc .inlinecode .id { + color: rgb(30%,30%,70%); +} + +.inlinecodenm { + display: inline; + color: #444444; +} + +.doc .code { + display: inline; + font-size: 120%; + color: rgb(30%,30%,70%); + font-family: monospace } + +.comment { + display: inline; + font-family: monospace; + color: rgb(50%,50%,80%); +} + +.code { + display: block; +/* padding-left: 15px; */ + font-size: 110%; + font-family: monospace; + } + +table.infrule { + border: 0px; + margin-left: 50px; + margin-top: 10px; + margin-bottom: 10px; +} + +td.infrule { + font-family: monospace; + text-align: center; +/* color: rgb(35%,35%,70%); */ + padding: 0px; + line-height: 100%; +} + +tr.infrulemiddle hr { + margin: 1px 0 1px 0; +} + +.infrulenamecol { + color: rgb(60%,60%,60%); + font-size: 80%; + padding-left: 1em; + padding-bottom: 0.1em +} + +/* Pied de page */ + +#footer { font-size: 65%; + font-family: sans-serif; } + +/* Identifiers: <span class="id" title="...">) */ + +.id { display: inline; } + +.id[title="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[title="var"] { + color: rgb(40%,0%,40%); +} + +.id[title="variable"] { + color: rgb(40%,0%,40%); +} + +.id[title="definition"] { + color: rgb(0%,40%,0%); +} + +.id[title="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[title="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[title="instance"] { + color: rgb(0%,40%,0%); +} + +.id[title="projection"] { + color: rgb(0%,40%,0%); +} + +.id[title="method"] { + color: rgb(0%,40%,0%); +} + +.id[title="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[title="record"] { + color: rgb(0%,0%,80%); +} + +.id[title="class"] { + color: rgb(0%,0%,80%); +} + +.id[title="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */ + +.id[type="constructor"] { + color: rgb(60%,0%,0%); +} + +.id[type="var"] { + color: rgb(40%,0%,40%); +} + +.id[type="variable"] { + color: rgb(40%,0%,40%); +} + +.id[type="definition"] { + color: rgb(0%,40%,0%); +} + +.id[type="abbreviation"] { + color: rgb(0%,40%,0%); +} + +.id[type="lemma"] { + color: rgb(0%,40%,0%); +} + +.id[type="instance"] { + color: rgb(0%,40%,0%); +} + +.id[type="projection"] { + color: rgb(0%,40%,0%); +} + +.id[type="method"] { + color: rgb(0%,40%,0%); +} + +.id[type="inductive"] { + color: rgb(0%,0%,80%); +} + +.id[type="record"] { + color: rgb(0%,0%,80%); +} + +.id[type="class"] { + color: rgb(0%,0%,80%); +} + +.id[type="keyword"] { + color : #cf1d1d; +/* color: black; */ +} + +.inlinecode .id { + color: rgb(0%,0%,0%); +} + + +/* TOC */ + +#toc h2 { + padding: 10px; + background-color: rgb(60%,60%,100%); +} + +#toc li { + padding-bottom: 8px; +} + +/* Index */ + +#index { + margin: 0; + padding: 0; + width: 100%; +} + +#index #frontispiece { + margin: 1em auto; + padding: 1em; + width: 60%; +} + +.booktitle { font-size : 140% } +.authors { font-size : 90%; + line-height: 115%; } +.moreauthors { font-size : 60% } + +#index #entrance { + text-align: center; +} + +#index #entrance .spacer { + margin: 0 30px 0 30px; +} + +#index #footer { + position: absolute; + bottom: 0; +} + +.paragraph { + height: 0.75em; +} + +ul.doclist { + margin-top: 0em; + margin-bottom: 0em; +} diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css new file mode 100644 index 0000000000..32c0b33166 --- /dev/null +++ b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css @@ -0,0 +1,801 @@ +body +{ + background: white; + color:#444; + font:normal normal normal small/1.5em "Lucida Grande", Verdana, sans-serif; + margin:0; + padding:0; +} + +h2 +{ + font-size:150%; + font-weight:normal; + margin:20px 0 0; +} + +h3 +{ + font-size:130%; + font-weight:normal; +} + +a:link,a:visited +{ + color:#660403; + font-weight:normal; + text-decoration:none; +} + +a:hover +{ + color: red; + text-decoration:none; +} + +#container +{ + margin: 0; + padding: 0; + } + + /*----------header, logo and site name styles----------*/ + #headertop + { + display: block; + /* position:absolute; */ + min-width: 700px; + top: 0; + width: 100%; + height:30px; + z-index: 1; + background: transparent url('images/header_top.png') repeat-x; + } + + #header + { + min-width: 700px; + width: 100%; height:70px; + position: relative; + left: 0; top: 0; + background: transparent url('images/header_bot.png') repeat-x; + } + + #logo + { + float:left; + z-index: 2; + position: absolute; + top: -15px; + left: 0px; + } + + #logo img + { + border:0; + float:left; + } + + #logoWrapper + { + line-height:4em; + } + + #siteName + { + position: relative; + top: 10px; left: 80px; + color:#fff; + float:left; + font-size:350%; + } + + #siteName a + { + color:#fff; + text-decoration:none; + } + + #siteName a:hover + { + color:#ddd; + text-decoration:none; + } + + #siteSlogan + { + color:#eee; + float:left; + font-size:170%; + margin:50px 0 0 10px; + text-transform:lowercase; + white-space:nowrap; + } + + /*----------nav styles -- primary links in header----------*/ + + #nav +{ + position:absolute; right:0; + margin: 0; + padding: 5px; + } + +#nav ul + { + list-style:none outside none; + list-style-image:none; + margin:0; + padding:0; + } + + #nav li + { + display: inline; + margin: 0; padding: 4px; + } + + #nav li a + { + border:medium none; + color:#ccc; + font-weight:normal; + padding-left:10px; + padding-right:10px; + text-decoration:none; + } + + #nav li a:hover + { + background:#7B0505 none repeat; + border:medium none; + border-left:1px solid #ddd; + border-right:1px solid #ddd; + color:#fff; + padding: 6px 9px 5px 9px; + } + + +/************** FOOTER *******************/ + + +#footer +{ + background:transparent url('images/footer.png') repeat-x; + width:100%; + clear:both; + font-size:85%; + text-align:center; + /* position:fixed; */ + margin: 0; + padding: 0; +} + + +#nav-footer +{ + display: inline; + color:#444; + margin: 0; + padding: 0; + text-align:right; + } + +#nav-footer ul + { + list-style:none outside none; + list-style-image:none; + margin:0; + padding:0px; padding-right: 5px; + } + +#nav-footer li +{ + display:inline; padding: 4px; +} + + #nav-footer li a + { + border:medium none; + color:#ccc; + font-size: 11px; + font-weight:normal; + padding-left: 10px; + padding-right: 10px; + text-decoration:none; + } + + #nav-footer li a:hover + { + background:#7B0505 none repeat; + border:medium none; + border-left:1px solid #ddd; + border-right:1px solid #ddd; + color:#fff; + margin:0; + padding: 3px 9px 0px 9px; + } + + + /*----------main content----------*/ + #content + { + display: block; + position: static; + +/* min-width: 640px; */ + max-width: 800px; + + margin-left:40px; + margin-right:300px; + padding: 2ex 2ex; + + z-index:1; + } + +.content { + display: block; + position: relative; + + margin: 0; + padding: 0; +} + + /*----------sidebar styles----------*/ + #sidebarWrapper + { + /* background:transparent url('images/sidebar_bottom.jpg') no-repeat scroll left bottom;*/ + display:block; + position:fixed; + /* avant : top: 100px; right:0px*/ + top: 15px; /* 180 */ + right:0px; + left: auto; + + margin-right: 0px; + + /* avant + width: 12%; + min-width:80px; */ + + /* width: 18%; */ + /* min-*/ + width:270px; + + z-index:0; + overflow:hidden; + +/* ajout precedent:*/ +/* min-height:320px; + padding:10px; + background-image:url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/rttr340bis.png'); + background-repeat : repeat-x ;*/ + +/* last ajout */ + /* min-height:510px; */ /* 360 */ + padding-left:0px; + padding-right:0px; + padding-top:105px; /* 40 */ + padding-bottom:/*105px*/115px; + /* background:transparent url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/trig6b.png') no-repeat scroll left top; */ + background:transparent url('images/sidebarbot.png') no-repeat scroll right bottom; + + } + +#sidebar { + padding-left: 40px; + padding-top: 105px; + overflow: visible; + background:transparent url('images/sidebartop.png') no-repeat scroll right top; +} + +#sidebar .title +{ + /* avant :border-bottom:1px solid #eee;*/ + /* avant : color:#660403;*/ + color:#2D0102; + font-size:120%; + font-weight:bold; + line-height:19px; + margin:10px 0; +} + +/*----------page styles----------*/ +.pageTitle +{ + color:#2D0102; + font-size:220%; + margin:10px 0 20px; +} + +.mission +{ + background-color:#efefef; + border:solid 1px #ccc; + margin:0 0 10px 0; + padding:10px; +} + +.messages +{ + color:#C80000; + font-size:110%; + margin:10px 0; +} + +/*----------node styles----------*/ +.nodeTitle +{ + background: url('images/nodeTitle.gif') no-repeat 0 100%; + color:#9a0000; + font-size: 100%; + margin:0; +} + +.nodeTitle a +{ + color:#660403; + text-decoration:none; +} + +.nodeTitle a:hover +{ + color:#d00000; + text-decoration:none; +} + +.node +{ + margin:0 0 20px; +} + +.content p +{ + margin:10px 0; +} + +.submitted +{ + color:#a3a3a3; + font-size:70%; +} + +.nodeLinks +{ + font-size:95%; + margin:0; + padding:0; +} + +.taxonomy +{ + background:url('icons/tag_red.png') no-repeat 0 7px; + font-size:80%; + padding:0 0 5px 16px; +} + +/*----------comment styles----------*/ +.commentTitle +{ + Border-bottom:1px solid #ddd; + color:#9a0000; + font-size:130%; + margin:20px 0 0; +} + +.commentTitle a +{ + color:#660403; + text-decoration:none; +} + +.commentTitle a:hover +{ + color:#d00000; + text-decoration:none; +} + +.commentLinks +{ + background:#f7f7f7; + border:1px solid #e1e1e1; + color:#444; + font-size:95%; + margin:20px 0 30px; + padding:4px 0 4px 4px; +} + + +/*----------img styles----------*/ +img +{ + padding:3px; +} + +/*----------icons for links----------*/ +.comment_comments a +{ + background:url('icons/comment.png') no-repeat 0 2px; + padding-bottom:5px; + padding-left:20px; +} + +.node_read_more a +{ + background:url('icons/page_white_go.png') no-repeat; + padding-bottom:5px; + padding-left:20px; +} + +.comment_add a,.comment_reply a +{ + background:url('icons/comment_add.png') no-repeat; + padding-bottom:5px; + padding-left:20px; +} +.comment_delete a +{ + background:url('icons/comment_delete.png') no-repeat; + padding-bottom:5px; + padding-left:20px; +} + +.comment_edit a +{ + background:url('icons/comment_edit.png') no-repeat; + padding-bottom:5px; + padding-left:20px; +} + +/*----------TinyMCE editor----------*/ +body.mceContentBody +{ + background:#fff; + color:#000; + font-size:12px; +} + +body.mceContentBody a:link +{ + color:#ff0000; +} + +/*----------table styles----------*/ +table +{ + margin:1em 0; + width:100%; +} + +thead th +{ + border-bottom:2px solid #AAA; + color:#494949; + font-weight:bold; +} + +td,th +{ + padding:.3em 0 .5em; +} + +tr.even,tr.odd,tbody th +{ + border:solid #D5D6D7; + border-width:1px 0; +} + +tr.even +{ + background:#fff; +} + +td.region,td.module,td.container +{ + background:#D5D6D7; + border-bottom:1px solid #AAA; + border-top:1.5em solid #fff; + color:#455067; + font-weight:bold; +} + +tr:first-child td.region,tr:first-child td.module,tr:first-child td.container +{ + border-top-width:0; +} + +td.menu-disabled,td.menu-disabled a +{ + background-color:#D5C2C2; + color:#000; +} + +/*----------other styles----------*/ + +.block +{ + margin:5px 0 20px; +} + +.thumbnail,.preview +{ + border:1px solid #ccc; +} + +.lstlisting { + display: block; + font-family: monospace; + white-space: pre; + margin: 1em 0; +} +.center { + text-align: center; +} +.centered { + display: block-inline; +} + +/*----------download table------------*/ + +table.downloadtable +{ + width:90%; + margin-left:auto; + margin-right:auto; +} + +table.downloadtable td.downloadheader +{ +padding: 2px 1em; +font-weight: bold; +font-size: 120%; +color: white; +background: transparent url('images/header_bot.png') repeat-x; +/*background-color: #660403; */ +border: solid 2px white; +border-left: none; +} + +table.downloadtable td.downloadcategory +{ +padding: 2px 1em; +background-color: #dfbfbe; +text-indent: 0; +} + +table.downloadtable td.downloadsize +{ +text-indent: 0; +white-space: nowrap; +height: 52px; +} + +table.downloadtable td +{ +padding: 2px 1em; +background-color: #dfbfbe; +border-right: solid white 2px; +} + + +table.downloadtable td.downloadtopline +{ +border-top: solid white 2px; +} + +table.downloadtable td.downloadtoprightline +{ +border-top: solid 2px white; +border-right: solid 2px white; +} + +table.downloadtable td.downloadbottomline +{ +border-bottom: solid 2px white; +border-right: solid 2px white; +} + +table.downloadtable td.downloadbottomrightline +{ +border-bottom: solid 2px white; +border-right: solid 2px white; +} + +table.downloadtable td.downloadrightline +{ +border-right: solid 2px white; +} + +table.downloadtable td.downloadback +{ +background-color: #efe4e4; +} + +table.downloadtable td.downloadbottomback +{ +border-bottom: solid 2px white; +background-color: #efe4e4; +} + + +/*********** Normal text style ************/ + +p { + text-indent:3em; +} + +ul { + margin: 0px; + margin-left:4em; + padding: 0px; + list-style-type:square; +} + +li +{ + text-indent: 0px; + margin: 0px; + padding: 0px; +} + +tt { font-size: 1em; } + +pre { font-size: 1em; } + +/*********** Framework ***********/ +.framework +{ + display: block; + position:relative; + border:solid 1px #660033; + margin: 8ex 1em; /* 8ex 8ex 1em 1em; */ + padding: 0; +} + +.frameworkcontent +{ + position:relative; + left:0px; + + + margin: 0; + padding: .5ex 2em; + + text-indent: 2em; + text-align: justify; +} + + +.frameworklabel +{ + display: inline; + position:relative; + top:-1.3ex; + + margin-left:2ex; + padding-top:.4ex; + padding-bottom:.4ex; + padding-right:1ex; + padding-left:1ex; + + border: none; + background: white; + color: black; + + font-weight: bold; + font-size:115%; +} + +.frameworklinks { + display:block; + position:relative; + top:1.4ex; + + margin-right:2ex; + + text-align:right; + font-size:100% + } + +.frameworklinks ul +{ + display: inline; + padding: 0px 1ex; + + border: none; + background: white; +} + + +.frameworklinks li + { + display:inline; + padding: 1ex 0px; + } + + .frameworklinks li a +{ + border:medium none; + + margin: 0px 1ex; + padding-left:2px; + padding-right:3px; + + font-weight:normal; + text-decoration:none; + + color: #660003; +} + + .frameworklinks li a:hover + { + color: red; + + border: none; + } + +/* General flat lists */ +.flatlist li {display: inline} + +/* For sections in bycat.html */ +.bycatsection dt { + text-indent: 3em +} + +.bycatsection dt a +{ + font-weight: bold; + color:#444; +} + +/* footnote is used in the new contribution form */ +.footnote { + text-indent: 0pt; + font-size: 80%; + color: silver; + text-align: justify +} + +/****************** CoqIDE Screenshots *****************/ + + +.SCpager { + position:relative; + top:5px; + width:630px; + background: transparent url('images/header_bot.png') repeat-x; + padding:4px; +} + +.SCpagercontent { + width:390px; + position:relative; + margin-left:auto; + margin-right:auto; +} + +.SCthumb { + height:45px; + margin-left:2px; + margin-right:2px; +} + +.SCthumbselected { + height:55px; + margin-left:2px; + margin-right:2px; +} + +.SCcontent { + position:relative; + top:5px; + width:638px; + background-color: #dfbfbe; +} + +.SCscreenshot { + position:relative; + height:400px; + width:auto; + margin:15px auto 15px 19px; +} diff --git a/doc/common/styles/html/coqremote/styles.hva b/doc/common/styles/html/coqremote/styles.hva new file mode 100644 index 0000000000..a09dc4f85f --- /dev/null +++ b/doc/common/styles/html/coqremote/styles.hva @@ -0,0 +1,81 @@ +\renewcommand{\@meta}{ +\begin{rawhtml} +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/system/system.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/modules/user/user.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/style.css" /> +<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/coqdoc.css" /> +\end{rawhtml}} + +% for HeVeA + +\htmlhead{\begin{rawhtml} +<div id="container"> + +<div id="headertop"> +<div id="nav"> + <ul class="links-menu"> + <li><a href="/" class="active">Home</a></li> + <li><a href="/about-coq" title="More about coq">About Coq</a></li> + <li><a href="/download">Get Coq</a></li> + <li><a href="/documentation">Documentation</a></li> + <li><a href="/community">Community</a></li> + </ul> +</div> +</div> + +<div id="header"> +<div id="logoWrapper"> + <div id="logo"><a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a> + </div> + <div id="siteName"><a href="/" title="Home">The Coq Proof Assistant</a> + </div> +</div> +</div> + +<div id="content"> + +\end{rawhtml}} + +\htmlfoot{\begin{rawhtml} +<div id="sidebarWrapper"> + <div id="sidebar"> + <div class="block"> + <h2 class="title">Navigation</h2> + <div class="content"> + <ul class="menu"> + <li class="leaf"><a href="index.html">Cover</a></li> + <li class="leaf"><a href="toc.html">Table of contents</a></li> + <li class="leaf">Index + <ul class="menu"> + <li><a href="general-index.html">General</a></li> + <li><a href="command-index.html">Commands</a></li> + <li><a href="option-index.html">Options</a></li> + <li><a href="tactic-index.html">Tactics</a></li> + <li><a href="error-index.html">Errors</a></li> + </ul> + </li> + </ul> + </div> + </div> + </div> +</div> + +</div> + +<div id="footer"> +<div id="nav-footer"> + <ul class="links-menu-footer"> + <li><a href="mailto:coq-www_@_inria.fr">webmaster</a></li> + <li><a href="http://validator.w3.org/">xhtml valid</a></li> + <li><a href="http://jigsaw.w3.org/css-validator/">CSS valid</a></li> + </ul> + +</div> +</div> + +</div> +\end{rawhtml}} diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html new file mode 100644 index 0000000000..6053131045 --- /dev/null +++ b/doc/common/styles/html/simple/cover.html @@ -0,0 +1,61 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en"> + +<head> + +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<title>Reference Manual | The Coq Proof Assistant</title> + +<link rel="stylesheet" type="text/css" href="style.css" /> +<link rel="stylesheet" type="text/css" href="coqdoc.css" /> + +</head> + +<body> + +<div id="container"> +<div id="header"> +</div> + +<div id="content"> + +<br /> +<h1 style="text-align:center; font-weight:bold; font-size: 300%; line-height: 2ex">Reference Manual</h1> + +<h2 style="text-align:center; font-size: 120%">Version COQVERSION</h2> +<br /> + +<h2 style="text-align:center; font-size: 150%">The Coq Development Team</h2> +<br /><br /><br /> + + +<p style="text-indent:0pt">Copyright © INRIA 1999-2017</p> + +<p style="text-indent: 0pt">This material may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at <a href="http://www.opencontent.org/openpub">http://www.opencontent.org/openpub</a>). Options A and B are not elected.</p> + +</div> +</div> +</div> + +<div id="footer"> + +<div class="content"> +<ul class="menu"> + <li><a href="index.html">Cover</a></li> + <li><a href="toc.html">Table of contents</a></li> + <li><a href="general-index.html">General index</a></li> + <li><a href="command-index.html">Commands index</a></li> + <li><a href="option-index.html">Options index</a></li> + <li><a href="tactic-index.html">Tactics index</a></li> + <li><a href="error-index.html">Errors index</a></li> +</ul> +</div> + +</div> + +</div> + +</body> + +</html> diff --git a/doc/common/styles/html/simple/footer.html b/doc/common/styles/html/simple/footer.html new file mode 100644 index 0000000000..308b1d01b6 --- /dev/null +++ b/doc/common/styles/html/simple/footer.html @@ -0,0 +1,2 @@ +</body> +</html> diff --git a/doc/common/styles/html/simple/header.html b/doc/common/styles/html/simple/header.html new file mode 100644 index 0000000000..c350a8b9b5 --- /dev/null +++ b/doc/common/styles/html/simple/header.html @@ -0,0 +1,13 @@ +<!DOCTYPE html + PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> + +<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<link rel="stylesheet" href="coqdoc.css" type="text/css" /> +<title>The Coq Standard Library</title> +</head> + +<body> + diff --git a/doc/common/styles/html/simple/hevea.css b/doc/common/styles/html/simple/hevea.css new file mode 100644 index 0000000000..5f4edef6f1 --- /dev/null +++ b/doc/common/styles/html/simple/hevea.css @@ -0,0 +1,36 @@ + +.li-itemize{margin:1ex 0ex;} +.li-enumerate{margin:1ex 0ex;} +.dd-description{margin:0ex 0ex 1ex 4ex;} +.dt-description{margin:0ex;} +.toc{list-style:none;} +.thefootnotes{text-align:left;margin:0ex;} +.dt-thefootnotes{margin:0em;} +.dd-thefootnotes{margin:0em 0em 0em 2em;} +.footnoterule{margin:1em auto 1em 0px;width:50%;} +.caption{padding-left:2ex; padding-right:2ex; margin-left:auto; margin-right:auto} +.title{margin:2ex auto;text-align:center} +.center{text-align:center;margin-left:auto;margin-right:auto;} +.flushleft{text-align:left;margin-left:0ex;margin-right:auto;} +.flushright{text-align:right;margin-left:auto;margin-right:0ex;} +DIV TABLE{margin-left:inherit;margin-right:inherit;} +PRE{text-align:left;margin-left:0ex;margin-right:auto;} +BLOCKQUOTE{margin-left:4ex;margin-right:4ex;text-align:left;} +TD P{margin:0px;} +.boxed{border:1px solid black} +.textboxed{border:1px solid black} +.vbar{border:none;width:2px;background-color:black;} +.hbar{border:none;height:2px;width:100%;background-color:black;} +.hfill{border:none;height:1px;width:200%;background-color:black;} +.vdisplay{border-collapse:separate;border-spacing:2px;width:auto; empty-cells:show; border:2px solid red;} +.vdcell{white-space:nowrap;padding:0px;width:auto; border:2px solid green;} +.display{border-collapse:separate;border-spacing:2px;width:auto; border:none;} +.dcell{white-space:nowrap;padding:0px;width:auto; border:none;} +.dcenter{margin:0ex auto;} +.vdcenter{border:solid #FF8000 2px; margin:0ex auto;} +.minipage{text-align:left; margin-left:0em; margin-right:auto;} +.marginpar{border:solid thin black; width:20%; text-align:left;} +.marginparleft{float:left; margin-left:0ex; margin-right:1ex;} +.marginparright{float:right; margin-left:1ex; margin-right:0ex;} +.theorem{text-align:left;margin:1ex auto 1ex 0ex;} +.part{margin:2ex auto;text-align:center} diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css new file mode 100644 index 0000000000..d1b2ce1112 --- /dev/null +++ b/doc/common/styles/html/simple/style.css @@ -0,0 +1,13 @@ +#footer { + border-top: solid black 1pt; + text-align: center; + text-indent: 0pt; +} + +.menu { } +.menu li { + display: inline; + margin: 0pt; + padding: .5ex 1em; + list-style: none +} diff --git a/doc/common/styles/html/simple/styles.hva b/doc/common/styles/html/simple/styles.hva new file mode 100644 index 0000000000..20d0d4dd0a --- /dev/null +++ b/doc/common/styles/html/simple/styles.hva @@ -0,0 +1,46 @@ +\renewcommand{\@meta}{ +\begin{rawhtml} +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> + +<link rel="stylesheet" type="text/css" href="style.css" /> +<link rel="stylesheet" type="text/css" href="coqdoc.css" /> +<link rel="stylesheet" type="text/css" href="hevea.css" /> + +\end{rawhtml}} + +% for HeVeA + +\htmlhead{\begin{rawhtml} + +<div id="container"> + +<div id="header"> +<h1>Coq Reference Manual</h1> +</div> + +<div id="content"> + +\end{rawhtml}} + +\htmlfoot{\begin{rawhtml} + +<div id="footer"> + +<div class="content"> +<ul class="menu"> + <li><a href="index.html">Cover</a></li> + <li><a href="toc.html">Table of contents</a></li> + <li><a href="general-index.html">General index</a></li> + <li><a href="command-index.html">Commands index</a></li> + <li><a href="option-index.html">Options index</a></li> + <li><a href="tactic-index.html">Tactics index</a></li> + <li><a href="error-index.html">Errors index</a></li> +</ul> + +</div> +</div> + +</div> +</div> +\end{rawhtml}} + diff --git a/doc/common/title.tex b/doc/common/title.tex new file mode 100644 index 0000000000..76e50f65d2 --- /dev/null +++ b/doc/common/title.tex @@ -0,0 +1,72 @@ +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% File title.tex +% Page formatting commands +% Macro \coverpage +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +%\setlength{\marginparwidth}{0pt} +%\setlength{\oddsidemargin}{0pt} +%\setlength{\evensidemargin}{0pt} +%\setlength{\marginparsep}{0pt} +%\setlength{\topmargin}{0pt} +%\setlength{\textwidth}{16.9cm} +%\setlength{\textheight}{22cm} +%\usepackage{fullpage} + +%\newcommand{\printingdate}{\today} +%\newcommand{\isdraft}{\Large\bf\today\\[20pt]} +%\newcommand{\isdraft}{\vspace{20pt}} + +\newcommand{\coverpage}[3]{ +\thispagestyle{empty} +\begin{center} +\bfseries % for the rest of this page, until \end{center} +\Huge +The Coq Proof Assistant\\[12pt] +#1\\[20pt] +\Large\today\\[20pt] +Version \coqversion\footnote[1]{This research was partly supported by IST working group ``Types''} + +\vspace{0pt plus .5fill} +#2 +\par\vfill +$\pi r^2$ Project (formerly LogiCal, then TypiCal) + +\vspace*{15pt} +\end{center} +\newpage + +\thispagestyle{empty} +\hbox{}\vfill % without \hbox \vfill does not work at the top of the page +\begin{flushleft} +%BEGIN LATEX +V\coqversion, \today +\par\vspace{20pt} +%END LATEX +\copyright INRIA 1999-2004 ({\Coq} versions 7.x) + +\copyright INRIA 2004-2017 ({\Coq} versions 8.x) + +#3 +\end{flushleft} +} % end of \coverpage definition + + +% \newcommand{\shorttitle}[1]{ +% \begin{center} +% \begin{huge} +% \begin{bf} +% The Coq Proof Assistant\\ +% \vspace{10pt} +% #1\\ +% \end{bf} +% \end{huge} +% \end{center} +% \vspace{5pt} +% } + +% Local Variables: +% mode: LaTeX +% TeX-master: "" +% End: + |