aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc
ModeNameSize
-rw-r--r--build-system.dev.txt5136logplain
-rw-r--r--build-system.txt11806logplain
-rw-r--r--changes.txt21833logplain
-rw-r--r--cic.dtd5562logplain
-rw-r--r--debugging.txt3089logplain
-rw-r--r--extensions.txt715logplain
-rw-r--r--minicoq.tex2947logplain
-rw-r--r--naming-conventions.tex20367logplain
-rw-r--r--newsyntax.tex24569logplain
-rw-r--r--notes-on-conversion2573logplain
-rw-r--r--patch.ocaml-3.10.drop.rectypes1155logplain
-rw-r--r--perf-analysis4638logplain
-rw-r--r--style.txt1623logplain
-rw-r--r--translate.txt16039logplain
-rw-r--r--universes.txt832logplain
-rw-r--r--versions-history.tex11035logplain