aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2184logplain
-rw-r--r--Cases.tex23563logplain
-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.tex67747logplain
-rw-r--r--RefMan-coi.tex16319logplain
-rw-r--r--RefMan-com.tex8922logplain
-rw-r--r--RefMan-ext.tex40404logplain
-rw-r--r--RefMan-gal.tex59961logplain
-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.tex34811logplain
-rw-r--r--RefMan-mod.tex10580logplain
-rw-r--r--RefMan-modr.tex15263logplain
-rw-r--r--RefMan-oth.tex28503logplain
-rw-r--r--RefMan-pre.tex27815logplain
-rw-r--r--RefMan-pro.tex12478logplain
-rw-r--r--RefMan-syn.tex39829logplain
-rw-r--r--RefMan-tac.tex115515logplain
-rw-r--r--RefMan-tacex.tex33510logplain
-rw-r--r--RefMan-tus.tex82611logplain
-rw-r--r--RefMan-uti.tex10557logplain
-rw-r--r--Reference-Manual.tex2949logplain
-rw-r--r--Setoid.tex24072logplain
-rw-r--r--biblio.bib41553logplain
-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