aboutsummaryrefslogtreecommitdiff
path: root/doc
ModeNameSize
-rw-r--r--.cvsignore753logplain
-rw-r--r--AddRefMan-pre.tex1591logplain
-rwxr-xr-xAnomalies.tex1060logplain
-rw-r--r--Cases.tex22025logplain
-rwxr-xr-xChanges.tex22686logplain
-rwxr-xr-xChangesV6-2.tex30331logplain
-rw-r--r--ChangesV6-3-1.tex4374logplain
-rw-r--r--ChangesV6-3.tex11420logplain
-rw-r--r--Coercion.tex14665logplain
-rwxr-xr-xExtraction.tex8785logplain
-rwxr-xr-xLibrary.tex1975logplain
-rw-r--r--Makefile.in8114logplain
-rwxr-xr-xNatural.tex11933logplain
-rwxr-xr-xOmega.tex6812logplain
-rw-r--r--Polynom.tex18980logplain
-rw-r--r--Program.tex32447logplain
-rw-r--r--Programs.tex32401logplain
-rwxr-xr-xREADME1841logplain
-rwxr-xr-xRecursive-Definition.tex8573logplain
-rwxr-xr-xRefMan-add.tex2086logplain
-rwxr-xr-xRefMan-cas.tex24675logplain
-rwxr-xr-xRefMan-cic.tex54919logplain
-rwxr-xr-xRefMan-coi.tex16273logplain
-rwxr-xr-xRefMan-com.tex7081logplain
-rw-r--r--RefMan-cover.tex1605logplain
-rw-r--r--RefMan-ext.tex24367logplain
-rw-r--r--RefMan-gal.tex44163logplain
-rwxr-xr-xRefMan-ind.tex17481logplain
-rwxr-xr-xRefMan-int.tex5684logplain
-rwxr-xr-xRefMan-lib.tex27555logplain
-rw-r--r--RefMan-ltac.tex27869logplain
-rw-r--r--RefMan-oth.tex25113logplain
-rwxr-xr-xRefMan-pre.tex18564logplain
-rwxr-xr-xRefMan-pro.tex10754logplain
-rwxr-xr-xRefMan-syn.tex64510logplain
-rw-r--r--RefMan-tac.tex82447logplain
-rw-r--r--RefMan-tacex.tex17570logplain
-rwxr-xr-xRefMan-tus.tex73088logplain
-rwxr-xr-xRefMan-uti.tex11165logplain
-rw-r--r--Reference-Manual.tex2181logplain
-rw-r--r--Tutorial-cover.tex1625logplain
-rwxr-xr-xTutorial.tex58046logplain
-rwxr-xr-xbiblio.bib36010logplain
-rw-r--r--book-html.sty2536logplain
-rwxr-xr-xconfigure30591logplain
-rw-r--r--configure.in1484logplain
-rw-r--r--coq-html.sty221logplain
-rw-r--r--discussion-syntaxe.txt8124logplain
-rw-r--r--headers.tex2917logplain
-rwxr-xr-xmacros.tex13300logplain
-rw-r--r--syntax.txt1790logplain
-rwxr-xr-xtitle.tex1464logplain