diff options
| author | Pierre-Marie Pédrot | 2018-06-07 06:29:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-07 06:29:00 +0200 |
| commit | f2b28f819c16ad773ab5a2e426e3c0a478cbfdef (patch) | |
| tree | dd7e83407bc35a70b392e93d68b10df1b12343b1 /kernel/mod_subst.ml | |
| parent | 82f18a32e4740c1429ac62506faff83955423417 (diff) | |
| parent | 387ed00319d7a7e8edb3644903086d2cd91eb9c7 (diff) | |
Merge PR #7706: Fix wrong deprecation msg
Diffstat (limited to 'kernel/mod_subst.ml')
0 files changed, 0 insertions, 0 deletions