diff options
| author | Pierre-Marie Pédrot | 2021-03-25 15:02:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-25 15:12:53 +0100 |
| commit | 4a865fbce27d2b5ba0824ad52db0fea36ede0a9e (patch) | |
| tree | c0ac404bee392afe92bbfab3403cb1ddf3d59b43 /kernel/nativecode.ml | |
| parent | d328a04d5e533a8591dfb3f2fa3d0e0852037f33 (diff) | |
Fix the redeclaration check for Ltac2 entry points.
Fixes #14003: Ltac2 redefinition check is broken.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions