diff options
| author | Gaëtan Gilbert | 2018-10-11 16:23:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | 0fa0ad02cb17a19edcd81efc8e41ccdd4f37ffaf (patch) | |
| tree | f7080975ced78150cb62b8bed29756a442406729 /dev/doc | |
| parent | 41072ec0482aa18a2a0ccc07814f672f7f85a7bd (diff) | |
Remove is_universe_polymorphism in funind
Funind doesn't support polymorphism.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions