diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-07 16:51:17 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-07 16:51:17 +0200 |
commit | a2615bc47ed022ed4466741af3d4a29d45d05950 (patch) | |
tree | ebbab72e7e5de11231fc84adbd6f079e99a824da /kernel/mod_subst.mli | |
parent | f4de78b048f6567f1e1fdd553b4f7ada0e0707b8 (diff) |
Fix bug #5125: Bad error message when attempting to use where with Class.
Diffstat (limited to 'kernel/mod_subst.mli')
0 files changed, 0 insertions, 0 deletions