aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2306logplain
-rw-r--r--Cases.tex25175logplain
-rw-r--r--Classes.tex15455logplain
-rw-r--r--Coercion.tex18455logplain
-rw-r--r--Extraction.tex24376logplain
-rw-r--r--Helm.tex13834logplain
-rw-r--r--Micromega.tex9442logplain
-rw-r--r--Natural.tex11945logplain
-rw-r--r--Omega.tex6830logplain
-rw-r--r--Polynom.tex40872logplain
-rw-r--r--Program.tex11778logplain
-rw-r--r--RefMan-add.tex2589logplain
-rw-r--r--RefMan-cic.tex76285logplain
-rw-r--r--RefMan-coi.tex16346logplain
-rw-r--r--RefMan-com.tex13965logplain
-rw-r--r--RefMan-decl.tex23079logplain
-rw-r--r--RefMan-ext.tex58648logplain
-rw-r--r--RefMan-gal.tex60966logplain
-rw-r--r--RefMan-ide.tex14758logplain
-rw-r--r--RefMan-ind.tex18635logplain
-rw-r--r--RefMan-int.tex6711logplain
-rw-r--r--RefMan-lib.tex32676logplain
-rw-r--r--RefMan-ltac.tex44813logplain
-rw-r--r--RefMan-mod.tex10657logplain
-rw-r--r--RefMan-modr.tex14788logplain
-rw-r--r--RefMan-oth.tex44612logplain
-rw-r--r--RefMan-pre.tex33841logplain
-rw-r--r--RefMan-pro.tex14080logplain
-rw-r--r--RefMan-syn.tex43905logplain
-rw-r--r--RefMan-tac.tex163616logplain
-rw-r--r--RefMan-tacex.tex44736logplain
-rw-r--r--RefMan-tus.tex82857logplain
-rw-r--r--RefMan-uti.tex10863logplain
-rw-r--r--Reference-Manual.tex3561logplain
-rw-r--r--Setoid.tex33397logplain
-rw-r--r--biblio.bib38272logplain
-rw-r--r--coqdoc.tex17436logplain
-rw-r--r--coqide-queries.png27316logplain
-rw-r--r--coqide.png20953logplain
-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