diff options
| author | Hugo Herbelin | 2018-03-28 15:27:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-03-28 20:50:20 +0200 |
| commit | e22add7d893bdc52bc123c671e839ce8eeabd3c4 (patch) | |
| tree | 620eb0c43445a9541d2806176012d20f508cfd2f /pretyping/patternops.ml | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Glob_ops: cosmetic renaming to reflect the type of objects.
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions