aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
ModeNameSize
-rw-r--r--AddRefMan-pre.tex2341logplain
-rw-r--r--AsyncProofs.tex11170logplain
-rw-r--r--CanonicalStructures.tex15616logplain
-rw-r--r--Cases.tex27513logplain
-rw-r--r--Classes.tex24322logplain
-rw-r--r--Coercion.tex19045logplain
-rw-r--r--Extraction.tex24987logplain
-rw-r--r--Micromega.tex11378logplain
-rw-r--r--Misc.tex2009logplain
-rw-r--r--Nsatz.tex4030logplain
-rw-r--r--Omega.tex6818logplain
-rw-r--r--Polynom.tex29951logplain
-rw-r--r--Program.tex14159logplain
-rw-r--r--RefMan-cic.tex87346logplain
-rw-r--r--RefMan-com.tex14451logplain
-rw-r--r--RefMan-ext.tex79734logplain
-rw-r--r--RefMan-gal.tex64998logplain
-rw-r--r--RefMan-ide.tex13064logplain
-rw-r--r--RefMan-int.tex6509logplain
-rw-r--r--RefMan-lib.tex32693logplain
-rw-r--r--RefMan-ltac.tex66352logplain
-rw-r--r--RefMan-mod.tex11749logplain
-rw-r--r--RefMan-modr.tex14810logplain
-rw-r--r--RefMan-oth.tex50933logplain
-rw-r--r--RefMan-pre.tex66192logplain
-rw-r--r--RefMan-pro.tex20816logplain
-rw-r--r--RefMan-sch.tex13407logplain
-rw-r--r--RefMan-ssr.tex197164logplain
-rw-r--r--RefMan-syn.tex50075logplain
-rw-r--r--RefMan-tac.tex201062logplain
-rw-r--r--RefMan-tacex.tex30388logplain
-rw-r--r--RefMan-uti.tex22303logplain
-rw-r--r--Reference-Manual.tex4759logplain
-rw-r--r--Setoid.tex38540logplain
-rw-r--r--Universes.tex14291logplain
-rw-r--r--biblio.bib43090logplain
-rw-r--r--coq-listing.tex4216logplain
-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.html188logplain
-rw-r--r--menu.html955logplain