diff options
| author | Maxime Dénès | 2016-05-02 17:11:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-05-04 10:20:17 +0200 |
| commit | 1dd8d826592507046b35128800578149021dab4c (patch) | |
| tree | faf1974949f2e6a44d2193003131c8275794b748 /kernel/nativecode.ml | |
| parent | 9173d3b0c4127e8217e93f8aad8ccba94037b486 (diff) | |
Fix for #4603, part 3: definitions inside proofs not handled properly by coqc.
Patch by Matthieu, Enrico and myself.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions