diff options
| author | Hugo Herbelin | 2015-09-16 21:44:47 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-16 22:05:15 +0200 |
| commit | 16db94e6c142217a81cc78be8788137617c24de7 (patch) | |
| tree | c52543ec1759d53f3bc14ca28f789d5bae9846b5 /kernel/nativecode.mli | |
| parent | 498cbad3e5e5d69d2ee771f90de45c0fe28cc494 (diff) | |
In pat/constr introduction patterns, fixing in a better way clearing problems
of temporary hypotheses than 76f27140e6e34 did.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions