diff options
author | 2015-11-22 17:38:18 +0100 | |
---|---|---|
committer | 2015-12-05 08:58:19 +0100 | |
commit | f22ad605a14eb14d11b0a1615f7014f2dca3b483 (patch) | |
tree | dd5e6675dcc46209f1ac33dad40292e85450ff1f /plugins/funind/recdef.ml | |
parent | f4002e6c85f575fc8451adb80dba705795f0a0c9 (diff) |
An example in centralizing similar functions to a common place so that
cleaning the interfaces is eventually easier. Here, adding
find_mrectype_vect to simplify vnorm.ml.
Diffstat (limited to 'plugins/funind/recdef.ml')
0 files changed, 0 insertions, 0 deletions