aboutsummaryrefslogtreecommitdiff
path: root/doc
ModeNameSize
-rw-r--r--.cvsignore966logplain
-rw-r--r--AddRefMan-pre.tex2219logplain
-rwxr-xr-xAnomalies.tex1060logplain
-rw-r--r--Cases.tex24318logplain
-rw-r--r--Changes.html5018logplain
-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.tex16514logplain
-rw-r--r--Correctness.tex32580logplain
-rwxr-xr-xExtraction.tex22851logplain
-rwxr-xr-xLibrary.tex2023logplain
-rw-r--r--Makefile11184logplain
-rwxr-xr-xNatural.tex11933logplain
-rwxr-xr-xOmega.tex6835logplain
-rw-r--r--Polynom.tex18986logplain
-rw-r--r--Program.tex32432logplain
-rwxr-xr-xREADME1810logplain
-rwxr-xr-xRecursive-Definition.tex8573logplain
-rwxr-xr-xRefMan-add.tex2086logplain
-rwxr-xr-xRefMan-cas.tex23870logplain
-rwxr-xr-xRefMan-cic.tex55369logplain
-rwxr-xr-xRefMan-coi.tex16319logplain
-rwxr-xr-xRefMan-com.tex7608logplain
-rw-r--r--RefMan-cover.tex1605logplain
-rw-r--r--RefMan-ext.tex35782logplain
-rw-r--r--RefMan-gal.tex46433logplain
-rwxr-xr-xRefMan-ind.tex17530logplain
-rwxr-xr-xRefMan-int.tex5683logplain
-rwxr-xr-xRefMan-lib.tex30600logplain
-rw-r--r--RefMan-ltac.tex28500logplain
-rw-r--r--RefMan-mod.tex8980logplain
-rw-r--r--RefMan-modr.tex13861logplain
-rw-r--r--RefMan-oth.tex27647logplain
-rwxr-xr-xRefMan-pre.tex25175logplain
-rwxr-xr-xRefMan-pro.tex12262logplain
-rwxr-xr-xRefMan-syn.tex85592logplain
-rw-r--r--RefMan-tac.tex100277logplain
-rw-r--r--RefMan-tacex.tex21065logplain
-rwxr-xr-xRefMan-tus.tex82611logplain
-rwxr-xr-xRefMan-uti.tex11350logplain
-rw-r--r--RefMan.txt2240logplain
-rw-r--r--Reference-Manual.tex2307logplain
-rw-r--r--Setoid.tex4908logplain
-rw-r--r--Tutorial-cover.tex1625logplain
-rwxr-xr-xTutorial.tex58350logplain
-rwxr-xr-xbiblio.bib39268logplain
-rw-r--r--book-html.sty2556logplain
-rw-r--r--coq-html.sty221logplain
-rw-r--r--cover.html839logplain
-rw-r--r--discussion-syntaxe.txt10648logplain
-rw-r--r--faq.tex25355logplain
-rw-r--r--headers.tex2911logplain
-rwxr-xr-xmacros.tex14985logplain
-rw-r--r--syntax.txt1790logplain
-rwxr-xr-xtitle.tex1456logplain
-rwxr-xr-xtov849logplain
-rw-r--r--tradv8.ml42748logplain
-rw-r--r--v8.txt656logplain