aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
ModeNameSize
-rw-r--r--.cvsignore8logplain
-rw-r--r--Makefile998logplain
-rw-r--r--ast.ml1254logplain
-rwxr-xr-xcheck-grammar1211logplain
-rw-r--r--intro.tex1260logplain
-rw-r--r--kernel.dep.ps13809logplain
-rw-r--r--lex.mll1640logplain
-rw-r--r--library.dep.ps11311logplain
-rw-r--r--macros.tex153logplain
-rw-r--r--memo-v8.tex9769logplain
-rw-r--r--minicoq.tex2947logplain
-rw-r--r--newsyntax.tex24569logplain
-rw-r--r--parse.ml4754logplain
-rw-r--r--parsing.dep.ps13040logplain
-rw-r--r--preamble.tex187logplain
-rw-r--r--pretyping.dep.ps14236logplain
-rw-r--r--proofs.dep.ps8805logplain
-rw-r--r--syntax-v8.tex39359logplain
-rw-r--r--syntax.mly5236logplain
-rw-r--r--tactics.dep.ps12719logplain
-rw-r--r--toplevel.dep.ps13499logplain