diff options
| author | Hugo Herbelin | 2015-04-02 18:41:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-21 15:56:34 +0200 |
| commit | ce6bbd05b7d741750228956a7e045cb202ec0e74 (patch) | |
| tree | 317c23b46d0bf5d6a1a99a5f7ac369da6e5aa0df /pretyping/patternops.ml | |
| parent | a33f7ad548ed312a2665c87baca9fb7b233e8cbf (diff) | |
Some dead code.
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions