aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
ModeNameSize
-rw-r--r--.cvsignore8logplain
-rw-r--r--Makefile1012logplain
-rw-r--r--ast.ml1254logplain
-rwxr-xr-xcheck-grammar1211logplain
-rw-r--r--interp.dep.ps10267logplain
-rw-r--r--intro.tex1260logplain
-rw-r--r--kernel.dep.ps24327logplain
-rw-r--r--lex.mll1640logplain
-rw-r--r--library.dep.ps14231logplain
-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.ps18827logplain
-rw-r--r--preamble.tex187logplain
-rw-r--r--pretyping.dep.ps21144logplain
-rw-r--r--proofs.dep.ps11082logplain
-rw-r--r--syntax-v8.tex40333logplain
-rw-r--r--syntax.mly5236logplain
-rw-r--r--tactics.dep.ps16644logplain
-rw-r--r--toplevel.dep.ps16558logplain