diff options
| author | coqbot-app[bot] | 2020-11-15 16:11:29 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-15 16:11:29 +0000 |
| commit | 93ee64000d4e121718b4735468626b481b2533bc (patch) | |
| tree | dd7fdfb6a7b1e2a41fc55fb811d8ea234862bbfb /kernel/nativecode.ml | |
| parent | 010dfd516839b901ce8e69dffc0c3751564a8ad6 (diff) | |
| parent | 3687c3fdcf2edd7b8e7f7408d9a8ee8706fd16a9 (diff) | |
Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly
Reviewed-by: ejgallego
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions