diff options
| author | herbelin | 2003-11-01 22:59:45 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-01 22:59:45 +0000 |
| commit | 504268e99ab32f8da836e88ec681c3d0432aaf24 (patch) | |
| tree | 6c78f89d6635a72bd2027d6a0192ddb0b37735da | |
| parent | b2dbc89b58adbb38d950f0c29b9c3046773675c4 (diff) | |
Ajout CPatNotation, PrintVisibility
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4766 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 9a0ecced4b..58eaf292a6 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -257,7 +257,8 @@ let rec xlate_match_pattern = CT_pattern_as (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id)) | CPatDelimiters(_, _, _) -> xlate_error "CPatDelimitors" - | CPatNumeral(_,_) -> xlate_error "CPatNumeral";; + | CPatNumeral(_,_) -> xlate_error "CPatNumeral" + | CPatNotation _ -> xlate_error "CPatNotation";; @@ -1462,6 +1463,7 @@ let xlate_vernac = | PrintModule _ -> xlate_error "TODO: Print Module" | PrintScopes -> xlate_error "TODO: Print Scopes" | PrintScope _ -> xlate_error "TODO: Print Scope" + | PrintVisibility _ -> xlate_error "TODO: Print Visibility" | PrintAbout _ -> xlate_error "TODO: Print About") | VernacBeginSection id -> CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id)) |