aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2184logplain
-rw-r--r--Cases.tex23555logplain
-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.tex17076logplain
-rw-r--r--RefMan-add.tex2086logplain
-rw-r--r--RefMan-cas.tex23870logplain
-rw-r--r--RefMan-cic.tex63819logplain
-rw-r--r--RefMan-coi.tex16319logplain
-rw-r--r--RefMan-com.tex8922logplain
-rw-r--r--RefMan-ext.tex40404logplain
-rw-r--r--RefMan-gal.tex50913logplain
-rw-r--r--RefMan-ide.tex13598logplain
-rw-r--r--RefMan-ind.tex17530logplain
-rw-r--r--RefMan-int.tex6695logplain
-rw-r--r--RefMan-lib.tex31793logplain
-rw-r--r--RefMan-ltac.tex34796logplain
-rw-r--r--RefMan-mod.tex10580logplain
-rw-r--r--RefMan-modr.tex15263logplain
-rw-r--r--RefMan-oth.tex28503logplain
-rw-r--r--RefMan-pre.tex27640logplain
-rw-r--r--RefMan-pro.tex12478logplain
-rw-r--r--RefMan-syn.tex39829logplain
-rw-r--r--RefMan-tac.tex112506logplain
-rw-r--r--RefMan-tacex.tex33728logplain
-rw-r--r--RefMan-tus.tex82611logplain
-rw-r--r--RefMan-uti.tex10557logplain
-rw-r--r--Reference-Manual.tex2949logplain
-rw-r--r--Setoid.tex4931logplain
-rw-r--r--biblio.bib41275logplain
-rw-r--r--coqdoc.tex14844logplain
-rw-r--r--coqide-queries.png27316logplain
-rw-r--r--coqide.png20953logplain
-rw-r--r--cover.html1267logplain
-rw-r--r--headers.tex3503logplain
-rw-r--r--hevea.sty2685logplain
-rw-r--r--index.html837logplain