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.tex18998logplain
-rw-r--r--Program.tex17964logplain
-rw-r--r--RefMan-add.tex2086logplain
-rw-r--r--RefMan-cas.tex23870logplain
-rw-r--r--RefMan-cic.tex73716logplain
-rw-r--r--RefMan-coi.tex16319logplain
-rw-r--r--RefMan-com.tex9093logplain
-rw-r--r--RefMan-ext.tex41800logplain
-rw-r--r--RefMan-gal.tex61050logplain
-rw-r--r--RefMan-ide.tex14005logplain
-rw-r--r--RefMan-ind.tex17530logplain
-rw-r--r--RefMan-int.tex6695logplain
-rw-r--r--RefMan-lib.tex31793logplain
-rw-r--r--RefMan-ltac.tex41194logplain
-rw-r--r--RefMan-mod.tex10133logplain
-rw-r--r--RefMan-modr.tex15263logplain
-rw-r--r--RefMan-oth.tex32476logplain
-rw-r--r--RefMan-pre.tex27882logplain
-rw-r--r--RefMan-pro.tex12262logplain
-rw-r--r--RefMan-syn.tex41923logplain
-rw-r--r--RefMan-tac.tex120892logplain
-rw-r--r--RefMan-tacex.tex33510logplain
-rw-r--r--RefMan-tus.tex82611logplain
-rw-r--r--RefMan-uti.tex10557logplain
-rw-r--r--Reference-Manual.tex2951logplain
-rw-r--r--Setoid.tex24072logplain
-rw-r--r--biblio.bib41696logplain
-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