aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/dumpglob.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/dumpglob.ml')
-rw-r--r--interp/dumpglob.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 13ed65056..0197cf9ae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -72,7 +72,7 @@ open Decl_kinds
let type_of_logical_kind = function
| IsDefinition def ->
(match def with
- | Definition -> "def"
+ | Definition | Let -> "def"
| Coercion -> "coe"
| SubClass -> "subclass"
| CanonicalStructure -> "canonstruc"