summaryrefslogtreecommitdiff
path: root/dev/doc
ModeNameSize
-rw-r--r--changes.txt18026logplain
-rw-r--r--cic.dtd5562logplain
-rw-r--r--debugging.txt2594logplain
-rw-r--r--extensions.txt715logplain
-rw-r--r--header525logplain
-rw-r--r--minicoq.tex2947logplain
-rw-r--r--newsyntax.tex24569logplain
-rw-r--r--perf-analysis2300logplain
-rw-r--r--style.txt982logplain
-rw-r--r--translate.txt16039logplain
-rw-r--r--universes.txt832logplain