summaryrefslogtreecommitdiff
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2306logplain
-rw-r--r--Cases.tex25176logplain
-rw-r--r--Classes.tex15494logplain
-rw-r--r--Coercion.tex19094logplain
-rw-r--r--Extraction.tex21264logplain
-rw-r--r--Helm.tex13834logplain
-rw-r--r--Micromega.tex10631logplain
-rw-r--r--Natural.tex11945logplain
-rw-r--r--Nsatz.tex4002logplain
-rw-r--r--Omega.tex6830logplain
-rw-r--r--Polynom.tex40612logplain
-rw-r--r--Program.tex12914logplain
-rw-r--r--RefMan-add.tex2580logplain
-rw-r--r--RefMan-cic.tex77033logplain
-rw-r--r--RefMan-coi.tex16340logplain
-rw-r--r--RefMan-com.tex13639logplain
-rw-r--r--RefMan-decl.tex23079logplain
-rw-r--r--RefMan-ext.tex66874logplain
-rw-r--r--RefMan-gal.tex63119logplain
-rw-r--r--RefMan-ide.tex13746logplain
-rw-r--r--RefMan-ind.tex18627logplain
-rw-r--r--RefMan-int.tex6702logplain
-rw-r--r--RefMan-lib.tex32372logplain
-rw-r--r--RefMan-ltac.tex46904logplain
-rw-r--r--RefMan-mod.tex11492logplain
-rw-r--r--RefMan-modr.tex14780logplain
-rw-r--r--RefMan-oth.tex47417logplain
-rw-r--r--RefMan-pre.tex44776logplain
-rw-r--r--RefMan-pro.tex15268logplain
-rw-r--r--RefMan-sch.tex12510logplain
-rw-r--r--RefMan-syn.tex46577logplain
-rw-r--r--RefMan-tac.tex168110logplain
-rw-r--r--RefMan-tacex.tex30119logplain
-rw-r--r--RefMan-tus.tex82824logplain
-rw-r--r--RefMan-uti.tex9584logplain
-rw-r--r--Reference-Manual.tex3962logplain
-rw-r--r--Setoid.tex33309logplain
-rw-r--r--biblio.bib39036logplain
-rw-r--r--coqdoc.tex17820logplain
-rw-r--r--coqide-queries.eps187058logplain
-rw-r--r--coqide-queries.png27316logplain
-rw-r--r--coqide.eps158733logplain
-rw-r--r--coqide.png20953logplain
-rw-r--r--headers.hva1487logplain
-rw-r--r--headers.sty3194logplain
-rw-r--r--hevea.sty2685logplain
-rw-r--r--index.html187logplain
-rw-r--r--menu.html837logplain