aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2184logplain
-rw-r--r--Cases.tex25128logplain
-rw-r--r--Coercion.tex18457logplain
-rw-r--r--Extraction.tex23040logplain
-rw-r--r--Helm.tex13846logplain
-rw-r--r--Natural.tex11933logplain
-rw-r--r--Omega.tex6831logplain
-rw-r--r--Polynom.tex27249logplain
-rw-r--r--Program.tex18380logplain
-rw-r--r--RefMan-add.tex2086logplain
-rw-r--r--RefMan-cas.tex23870logplain
-rw-r--r--RefMan-cic.tex74618logplain
-rw-r--r--RefMan-coi.tex16319logplain
-rw-r--r--RefMan-com.tex9093logplain
-rw-r--r--RefMan-ext.tex42697logplain
-rw-r--r--RefMan-gal.tex61036logplain
-rw-r--r--RefMan-ide.tex14005logplain
-rw-r--r--RefMan-ind.tex17530logplain
-rw-r--r--RefMan-int.tex6695logplain
-rw-r--r--RefMan-lib.tex31978logplain
-rw-r--r--RefMan-ltac.tex41485logplain
-rw-r--r--RefMan-mod.tex10133logplain
-rw-r--r--RefMan-modr.tex15263logplain
-rw-r--r--RefMan-oth.tex32476logplain
-rw-r--r--RefMan-pre.tex28739logplain
-rw-r--r--RefMan-pro.tex12710logplain
-rw-r--r--RefMan-syn.tex41923logplain
-rw-r--r--RefMan-tac.tex125597logplain
-rw-r--r--RefMan-tacex.tex33805logplain
-rw-r--r--RefMan-tus.tex82611logplain
-rw-r--r--RefMan-uti.tex10557logplain
-rw-r--r--Reference-Manual.tex2951logplain
-rw-r--r--Setoid.tex24121logplain
-rw-r--r--biblio.bib42294logplain
-rw-r--r--coqdoc.tex14903logplain
-rw-r--r--coqide-queries.png27316logplain
-rw-r--r--coqide.png20953logplain
-rw-r--r--cover.html1309logplain
-rw-r--r--headers.tex3503logplain
-rw-r--r--hevea.sty2685logplain
-rw-r--r--index.html187logplain
-rw-r--r--menu.html837logplain