diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 801f7208e4..e9995e5590 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1666,6 +1666,7 @@ let xlate_vernac = (* Modules and Module Types *) | VernacDeclareModule _ -> xlate_error "TODO: vernac" + | VernacDefineModule _ -> xlate_error "TODO: vernac" | VernacDeclareModuleType _ -> xlate_error "TODO: vernac" let rec xlate_vernac_list = |