aboutsummaryrefslogtreecommitdiff
path: root/doc
ModeNameSize
-rw-r--r--.cvsignore777logplain
-rw-r--r--AddRefMan-pre.tex1591logplain
-rwxr-xr-xAnomalies.tex1060logplain
-rw-r--r--Cases.tex22025logplain
-rwxr-xr-xChanges.tex25227logplain
-rwxr-xr-xChangesV6-2.tex30331logplain
-rw-r--r--ChangesV6-3-1.tex4374logplain
-rw-r--r--ChangesV6-3.tex11420logplain
-rw-r--r--Coercion.tex14698logplain
-rw-r--r--Correctness.tex32340logplain
-rwxr-xr-xExtraction.tex8749logplain
-rwxr-xr-xLibrary.tex2102logplain
-rw-r--r--Makefile9658logplain
-rwxr-xr-xNatural.tex11933logplain
-rwxr-xr-xOmega.tex6812logplain
-rw-r--r--Polynom.tex18969logplain
-rw-r--r--Program.tex32447logplain
-rwxr-xr-xREADME1841logplain
-rwxr-xr-xRecursive-Definition.tex8573logplain
-rwxr-xr-xRefMan-add.tex2086logplain
-rwxr-xr-xRefMan-cas.tex24675logplain
-rwxr-xr-xRefMan-cic.tex55161logplain
-rwxr-xr-xRefMan-coi.tex16273logplain
-rwxr-xr-xRefMan-com.tex7081logplain
-rw-r--r--RefMan-cover.tex1605logplain
-rw-r--r--RefMan-ext.tex25646logplain
-rw-r--r--RefMan-gal.tex44398logplain
-rwxr-xr-xRefMan-ind.tex17481logplain
-rwxr-xr-xRefMan-int.tex5684logplain
-rwxr-xr-xRefMan-lib.tex29379logplain
-rw-r--r--RefMan-ltac.tex27869logplain
-rw-r--r--RefMan-oth.tex24915logplain
-rwxr-xr-xRefMan-pre.tex18836logplain
-rwxr-xr-xRefMan-pro.tex11479logplain
-rwxr-xr-xRefMan-syn.tex65116logplain
-rw-r--r--RefMan-tac.tex86190logplain
-rw-r--r--RefMan-tacex.tex17570logplain
-rwxr-xr-xRefMan-tus.tex73088logplain
-rwxr-xr-xRefMan-uti.tex11165logplain
-rw-r--r--Reference-Manual.tex2184logplain
-rw-r--r--Tutorial-cover.tex1625logplain
-rwxr-xr-xTutorial.tex58046logplain
-rwxr-xr-xbiblio.bib36752logplain
-rw-r--r--book-html.sty2536logplain
-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:39:46 +0000