aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorbertot2004-02-23 13:05:32 +0000
committerbertot2004-02-23 13:05:32 +0000
commit6032ae1dfaf2f9313aad8277b44df1d9d0cc8d91 (patch)
tree3ac456d2676027c0965748d70151173a2142dde3
parent9c54f84cee8057fbb90fdfdee1eb7fa9faffbc4f (diff)
corrects the treatement of SubClass declarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5372 85f007b7-540e-0410-9357-904b9bb8a0f7
-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"