diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-15 01:04:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-15 01:12:53 +0200 |
| commit | e349809cf36289dc73249b2861007cc24e01bfa7 (patch) | |
| tree | 21421d0778bd9451ac71decf38e581e16ef8ac9a /interp/topconstr.mli | |
| parent | ec878d596f15ad2baa10395fffd3849df5597f78 (diff) | |
Still a problem with debug auto printing.
"msg_debug (mt())" is not identity, so we return back to how it was
done in 8.4, contracting a repeated pattern-matching into one.
Diffstat (limited to 'interp/topconstr.mli')
0 files changed, 0 insertions, 0 deletions