diff options
| author | Hugo Herbelin | 2016-09-03 11:45:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-09-03 11:46:15 +0200 |
| commit | 52b82dd42b93af6831df3bfea4822c6c8680a288 (patch) | |
| tree | 7a661eb53fb3e5eea29c0c85ab408c84caa05021 /kernel/nativecode.ml | |
| parent | af2df1ada04da94a41a400c637788db461a532d9 (diff) | |
Fixing what is probably a typo in Strict Proofs mode (#5062).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions