aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2306logplain
-rw-r--r--AsyncProofs.tex7566logplain
-rw-r--r--CanonicalStructures.tex14948logplain
-rw-r--r--Cases.tex27461logplain
-rw-r--r--Classes.tex15564logplain
-rw-r--r--Coercion.tex19099logplain
-rw-r--r--Extraction.tex23350logplain
-rw-r--r--Helm.tex13942logplain
-rw-r--r--Micromega.tex10651logplain
-rw-r--r--Misc.tex1974logplain
-rw-r--r--Natural.tex11907logplain
-rw-r--r--Nsatz.tex4002logplain
-rw-r--r--Omega.tex6831logplain
-rw-r--r--Polynom.tex29944logplain
-rw-r--r--Program.tex13382logplain
-rw-r--r--RefMan-add.tex2580logplain
-rw-r--r--RefMan-cic.tex78074logplain
-rw-r--r--RefMan-coi.tex16333logplain
-rw-r--r--RefMan-com.tex12114logplain
-rw-r--r--RefMan-decl.tex23069logplain
-rw-r--r--RefMan-ext.tex70255logplain
-rw-r--r--RefMan-gal.tex63690logplain
-rw-r--r--RefMan-ide.tex13291logplain
-rw-r--r--RefMan-ind.tex18626logplain
-rw-r--r--RefMan-int.tex6705logplain
-rw-r--r--RefMan-lib.tex32424logplain
-rw-r--r--RefMan-ltac.tex54464logplain
-rw-r--r--RefMan-mod.tex11816logplain
-rw-r--r--RefMan-modr.tex14780logplain
-rw-r--r--RefMan-oth.tex50538logplain
-rw-r--r--RefMan-pre.tex45660logplain
-rw-r--r--RefMan-pro.tex16676logplain
-rw-r--r--RefMan-sch.tex12526logplain
-rw-r--r--RefMan-syn.tex47209logplain
-rw-r--r--RefMan-tac.tex177152logplain
-rw-r--r--RefMan-tacex.tex30099logplain
-rw-r--r--RefMan-tus.tex82824logplain
-rw-r--r--RefMan-uti.tex9591logplain
-rw-r--r--Reference-Manual.tex4113logplain
-rw-r--r--Setoid.tex38435logplain
-rw-r--r--Universes.tex5161logplain
-rw-r--r--biblio.bib40574logplain
-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