diff options
| author | Hugo Herbelin | 2017-08-13 23:56:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-09-12 20:30:11 +0200 |
| commit | 2e1ae2cab5a4c103ecafe7ab71b77a7ee7589760 (patch) | |
| tree | e5a738d143161e4865fc84be75c9d998b47b5f1f /interp/notation_ops.ml | |
| parent | bc3b07f639f04295bc440f42d5aa2420c07ecee6 (diff) | |
Don't exclude a priori CLocalDef to be treated by ppconstr.ml.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions