diff options
author | 2018-05-23 13:34:46 +0200 | |
---|---|---|
committer | 2018-05-23 18:50:10 +0200 | |
commit | 33b5074f24270c202a9922f21d445c12cc6b3b3d (patch) | |
tree | 67d69b51caf3b7849e2d90d21e6ed7dc705d3249 /plugins/funind/glob_term_to_relation.ml | |
parent | 944f62d08b7d78bcb20dd12ba138891d432b5987 (diff) |
Collecting List.smart_* functions into a module List.Smart.
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
0 files changed, 0 insertions, 0 deletions