summaryrefslogtreecommitdiff
path: root/dev/doc
ModeNameSize
-rw-r--r--about-hints10721logplain
-rw-r--r--build-system.dev.txt5518logplain
-rw-r--r--build-system.txt5213logplain
-rw-r--r--changes.txt28660logplain
-rw-r--r--cic.dtd5562logplain
-rw-r--r--coq-src-description.txt2569logplain
-rw-r--r--debugging.txt2865logplain
-rw-r--r--extensions.txt723logplain
-rw-r--r--minicoq.tex2947logplain
-rw-r--r--naming-conventions.tex22808logplain
-rw-r--r--newsyntax.tex24842logplain
-rw-r--r--notes-on-conversion2573logplain
-rw-r--r--old_svn_branches.txt1345logplain
-rw-r--r--perf-analysis5715logplain
-rw-r--r--style.txt1638logplain
-rw-r--r--transition-V5.10-V6310logplain
-rw-r--r--transition-V6-V7395logplain
-rw-r--r--translate.txt16039logplain
-rw-r--r--unification.txt5269logplain
-rw-r--r--universes.txt634logplain
-rw-r--r--univpoly.txt12294logplain
-rw-r--r--versions-history.tex11034logplain