aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--contrib/interface/xlate.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 5359c69ade..8dc40b6a2c 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1358,8 +1358,8 @@ let xlate_thm x = CT_thm (match x with
let xlate_defn x = CT_defn (match x with
| (Local, Definition) -> "Local"
| (Global, Definition) -> "Definition"
- | (Global, Coercion) -> "SubClass"
- | (Local, Coercion) -> "Local SubClass"
+ | (Global, SubClass) -> "SubClass"
+ | (Local, SubClass) -> "Local SubClass"
| (Global,CanonicalStructure) -> "Canonical Structure"
| (Local, CanonicalStructure) ->
xlate_error "Local CanonicalStructure not parsed"