aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
ModeNameSize
-rw-r--r--.cvsignore957logplain
-rw-r--r--AddRefMan-pre.tex2220logplain
-rwxr-xr-xAnomalies.tex1060logplain
-rw-r--r--Cases.tex24734logplain
-rwxr-xr-xChanges.tex391logplain
-rwxr-xr-xChangesV6-2.tex30331logplain
-rw-r--r--ChangesV6-3-1.tex4374logplain
-rw-r--r--ChangesV6-3.tex11420logplain
-rwxr-xr-xChangesV7-0.tex26682logplain
-rw-r--r--Coercion.tex15976logplain
-rw-r--r--Correctness.tex32405logplain
-rwxr-xr-xExtraction.tex9331logplain
-rwxr-xr-xLibrary.tex2023logplain
-rw-r--r--Makefile10700logplain
-rwxr-xr-xNatural.tex11933logplain
-rwxr-xr-xOmega.tex6812logplain
-rw-r--r--Polynom.tex18969logplain
-rw-r--r--Program.tex32432logplain
-rwxr-xr-xREADME1811logplain
-rwxr-xr-xRecursive-Definition.tex8573logplain
-rwxr-xr-xRefMan-add.tex2086logplain
-rwxr-xr-xRefMan-cas.tex24675logplain
-rwxr-xr-xRefMan-cic.tex55491logplain
-rwxr-xr-xRefMan-coi.tex16273logplain
-rwxr-xr-xRefMan-com.tex7608logplain
-rw-r--r--RefMan-cover.tex1605logplain
-rw-r--r--RefMan-ext.tex31325logplain
-rw-r--r--RefMan-gal.tex46118logplain
-rwxr-xr-xRefMan-ind.tex17481logplain
-rwxr-xr-xRefMan-int.tex5684logplain
-rwxr-xr-xRefMan-lib.tex29741logplain
-rw-r--r--RefMan-ltac.tex25222logplain
-rw-r--r--RefMan-oth.tex29268logplain
-rwxr-xr-xRefMan-pre.tex19795logplain
-rwxr-xr-xRefMan-pro.tex12266logplain
-rwxr-xr-xRefMan-syn.tex67410logplain
-rw-r--r--RefMan-tac.tex91865logplain
-rw-r--r--RefMan-tacex.tex17744logplain
-rwxr-xr-xRefMan-tus.tex73088logplain
-rwxr-xr-xRefMan-uti.tex11165logplain
-rw-r--r--Reference-Manual.tex2269logplain
-rw-r--r--Setoid.tex4908logplain
-rw-r--r--Tutorial-cover.tex1625logplain
-rwxr-xr-xTutorial.tex58036logplain
-rwxr-xr-xbiblio.bib36812logplain
-rw-r--r--book-html.sty2556logplain
-rw-r--r--coq-html.sty221logplain
-rw-r--r--cover.html839logplain
-rw-r--r--discussion-syntaxe.txt8124logplain
-rw-r--r--headers.tex2911logplain
-rwxr-xr-xmacros.tex13453logplain
-rw-r--r--syntax.txt1790logplain
-rwxr-xr-xtitle.tex1456logplain