aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/notes-on-conversion.v
AgeCommit message (Collapse)Author
2019-03-15Remove clutter by moving historic unmaintained dev/doc files to an archive ↵Théo Zimmermann
subfolder.
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
This gives syntax highlighting in Coq-aware editors.