diff options
| author | herbelin | 2002-09-29 09:35:37 +0000 |
|---|---|---|
| committer | herbelin | 2002-09-29 09:35:37 +0000 |
| commit | caa93dd02540162150a7d048e36ca1c1dc9cb0d4 (patch) | |
| tree | 7e4be5ac526d60135b446abfac396989448c2fdc | |
| parent | fe612bc2d47bcdcb1166e3bbff688c68d55a449b (diff) | |
Complétion filtrage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3046 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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) -> |