diff options
author | 2018-06-22 14:08:49 +0200 | |
---|---|---|
committer | 2018-06-28 13:24:43 +0200 | |
commit | e7e3714f0fd0e791501acccca3317ed8175c4815 (patch) | |
tree | a50c12ccf3e22b7ef2ba25cdf330adc968b3d757 /kernel/modops.mli | |
parent | a8c4dee491fdd2426c623ad458ed15310295c93b (diff) |
Deprecate Environ.retroknowledge function in favor of the projection
Diffstat (limited to 'kernel/modops.mli')
0 files changed, 0 insertions, 0 deletions