diff options
| author | Théo Zimmermann | 2017-06-12 11:14:54 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-12 11:14:54 +0200 |
| commit | 76f97eac9e0b6eee76469b2a00a9c157caa3da8a (patch) | |
| tree | b6a076e12bae66fe62ef8b74b03a20989e3e23cb /interp/notation_ops.ml | |
| parent | 2253d2eb4f892f932332358be8537fdb5552ef87 (diff) | |
Remove more dead code (follow-up of previous commit).
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions