diff options
| author | Pierre-Marie Pédrot | 2014-11-09 23:45:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-09 23:46:51 +0100 |
| commit | 9fa45b3b3b67cf98abb3c246880b2c202c475947 (patch) | |
| tree | 16fd35d7ea6ac83fd3d57a6bb551ba77878d51c7 /kernel/nativelib.ml | |
| parent | 03b0c585e2b4946be6c529eb3359c3715ea312cb (diff) | |
Fixing bug #3803.
The Info layer was setting the required evarmap too eagerly, making the
tclWITHHOLE tactical accept terms with holes. The logging facility is
now inside the tclWITHHOLES.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions