diff options
Diffstat (limited to 'plugins/interface')
| -rw-r--r-- | plugins/interface/xlate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 627cd517c3..261bb0029c 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -2145,8 +2145,8 @@ let rec xlate_vernac = CT_coercion (local_opt, id_opt, xlate_ident id1, xlate_class id2, xlate_class id3) - (* Type Classes *) - | VernacDeclareInstance _|VernacContext _| + (* Type Classes *) + | VernacDeclareInstance _ | VernacDeclareClass _ | VernacContext _ | VernacInstance (_, _, _, _, _) -> xlate_error "TODO: Type Classes commands" |