diff options
| author | Pierre-Marie Pédrot | 2016-05-10 19:46:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-10 23:13:45 +0200 |
| commit | f2983cec3544473b18ebc4d4e3a20b941decd196 (patch) | |
| tree | 0f0d76b21c427a0e77688e6eba01e7657991fed4 /kernel/declareops.ml | |
| parent | bc3981687cd363820e35e5a2bd037d50e213f524 (diff) | |
Delimiting the use of unsafe code in Pcoq.
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions