diff options
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index a2620c67f7..d3d25534ce 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -3337,6 +3337,10 @@ let xlate_vernac = VernacTacticGrammar _|VernacVar _|VernacTime _|VernacNop|VernacComments _) -> xlate_error "TODO: vernac" + (* Modules and Module Types *) + | VernacDeclareModule _ -> xlate_error "TODO: vernac" + | VernacDeclareModuleType _ -> xlate_error "TODO: vernac" + let xlate_vernac_list = function | VernacList (v::l) -> |