aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2204logplain
-rw-r--r--Cases.tex25167logplain
-rw-r--r--Coercion.tex18457logplain
-rw-r--r--Extraction.tex23341logplain
-rw-r--r--Helm.tex13903logplain
-rw-r--r--Natural.tex11945logplain
-rw-r--r--Omega.tex6831logplain
-rw-r--r--Polynom.tex40840logplain
-rw-r--r--Program.tex10954logplain
-rw-r--r--RefMan-add.tex2589logplain
-rw-r--r--RefMan-cic.tex75184logplain
-rw-r--r--RefMan-coi.tex16346logplain
-rw-r--r--RefMan-com.tex9156logplain
-rw-r--r--RefMan-ext.tex50183logplain
-rw-r--r--RefMan-gal.tex59601logplain
-rw-r--r--RefMan-ide.tex14268logplain
-rw-r--r--RefMan-ind.tex18635logplain
-rw-r--r--RefMan-int.tex6719logplain
-rw-r--r--RefMan-lib.tex32232logplain
-rw-r--r--RefMan-ltac.tex43280logplain
-rw-r--r--RefMan-mod.tex10137logplain
-rw-r--r--RefMan-modr.tex15281logplain
-rw-r--r--RefMan-oth.tex37316logplain
-rw-r--r--RefMan-pre.tex28795logplain
-rw-r--r--RefMan-pro.tex14531logplain
-rw-r--r--RefMan-syn.tex42086logplain
-rw-r--r--RefMan-tac.tex129144logplain
-rw-r--r--RefMan-tacex.tex34583logplain
-rw-r--r--RefMan-tus.tex82909logplain
-rw-r--r--RefMan-uti.tex10894logplain
-rw-r--r--Reference-Manual.tex3419logplain
-rw-r--r--Setoid.tex24121logplain
-rw-r--r--biblio.bib35141logplain
-rw-r--r--coqdoc.tex15003logplain
-rw-r--r--coqide-queries.png27316logplain
-rw-r--r--coqide.png20953logplain
-rw-r--r--cover.html1309logplain
-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