aboutsummaryrefslogtreecommitdiff
path: root/dev/doc
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-05-10 19:46:39 +0200
committerPierre-Marie Pédrot2016-05-10 23:13:45 +0200
commitf2983cec3544473b18ebc4d4e3a20b941decd196 (patch)
tree0f0d76b21c427a0e77688e6eba01e7657991fed4 /dev/doc
parentbc3981687cd363820e35e5a2bd037d50e213f524 (diff)
Delimiting the use of unsafe code in Pcoq.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions