aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
ModeNameSize
-rw-r--r--build-system.dev.txt2982logplain
-rw-r--r--build-system.txt11866logplain
-rw-r--r--changes.txt18939logplain
-rw-r--r--cic.dtd5562logplain
-rw-r--r--debugging.txt2594logplain
-rw-r--r--extensions.txt715logplain
-rw-r--r--minicoq.tex2947logplain
-rw-r--r--newsyntax.tex24569logplain
-rw-r--r--notes-on-conversion2573logplain
-rw-r--r--perf-analysis4487logplain
-rw-r--r--style.txt982logplain
-rw-r--r--translate.txt16039logplain
-rw-r--r--universes.txt832logplain