summaryrefslogtreecommitdiff
path: root/dev/doc
ModeNameSize
-rw-r--r--about-hints10721logplain
-rw-r--r--build-system.dev.txt5892logplain
-rw-r--r--build-system.txt13575logplain
-rw-r--r--changes.txt24416logplain
-rw-r--r--cic.dtd5562logplain
-rw-r--r--debugging.txt3341logplain
-rw-r--r--extensions.txt715logplain
-rw-r--r--minicoq.tex2947logplain
-rw-r--r--naming-conventions.tex22809logplain
-rw-r--r--newsyntax.tex24569logplain
-rw-r--r--notes-on-conversion2573logplain
-rw-r--r--patch.ocaml-3.10.drop.rectypes1155logplain
-rw-r--r--perf-analysis5715logplain
-rw-r--r--style.txt1623logplain
-rw-r--r--translate.txt16039logplain
-rw-r--r--unification.txt5269logplain
-rw-r--r--universes.txt634logplain
-rw-r--r--versions-history.tex11035logplain