diff options
| author | Arnaud Spiwack | 2014-08-05 12:14:30 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:52:13 +0200 |
| commit | 076ac1757383cd9e3f505c3f958c1757087011ac (patch) | |
| tree | e962c04eb294689b901a87cfe5dab530d9c4fbfb /kernel/nativecode.ml | |
| parent | b19a845e7bbda10120a8a1f4b5cf92a057b5d10f (diff) | |
Properly declare uconstr as an argument for TACTIC EXTEND.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions