aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2311logplain
-rw-r--r--AsyncProofs.tex10756logplain
-rw-r--r--CanonicalStructures.tex15574logplain
-rw-r--r--Cases.tex27486logplain
-rw-r--r--Classes.tex24008logplain
-rw-r--r--Coercion.tex19014logplain
-rw-r--r--Extraction.tex23807logplain
-rw-r--r--Micromega.tex11347logplain
-rw-r--r--Misc.tex1974logplain
-rw-r--r--Nsatz.tex4003logplain
-rw-r--r--Omega.tex6791logplain
-rw-r--r--Polynom.tex29923logplain
-rw-r--r--Program.tex14073logplain
-rw-r--r--RefMan-add.tex2580logplain
-rw-r--r--RefMan-cic.tex84513logplain
-rw-r--r--RefMan-coi.tex16333logplain
-rw-r--r--RefMan-com.tex14010logplain
-rw-r--r--RefMan-decl.tex23081logplain
-rw-r--r--RefMan-ext.tex76452logplain
-rw-r--r--RefMan-gal.tex64797logplain
-rw-r--r--RefMan-ide.tex13429logplain
-rw-r--r--RefMan-ind.tex18626logplain
-rw-r--r--RefMan-int.tex6705logplain
-rw-r--r--RefMan-lib.tex32665logplain
-rw-r--r--RefMan-ltac.tex64686logplain
-rw-r--r--RefMan-mod.tex11749logplain
-rw-r--r--RefMan-modr.tex14781logplain
-rw-r--r--RefMan-oth.tex48935logplain
-rw-r--r--RefMan-pre.tex60464logplain
-rw-r--r--RefMan-pro.tex20950logplain
-rw-r--r--RefMan-sch.tex13261logplain
-rw-r--r--RefMan-syn.tex48260logplain
-rw-r--r--RefMan-tac.tex193375logplain
-rw-r--r--RefMan-tacex.tex30349logplain
-rw-r--r--RefMan-tus.tex82824logplain
-rw-r--r--RefMan-uti.tex11977logplain
-rw-r--r--Reference-Manual.tex4315logplain
-rw-r--r--Setoid.tex38510logplain
-rw-r--r--Universes.tex10445logplain
-rw-r--r--biblio.bib43090logplain
-rw-r--r--coqdoc.tex18448logplain
-rw-r--r--coqide-queries.png27316logplain
-rw-r--r--coqide.png20953logplain
-rw-r--r--headers.hva1489logplain
-rw-r--r--headers.sty3084logplain
-rw-r--r--hevea.sty2685logplain
-rw-r--r--index.html187logplain
-rw-r--r--menu.html955logplain