diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:44:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-12 14:44:43 +0000 |
| commit | 59d27909bc49a1ef65d6b03f2804f13dd47fda4f (patch) | |
| tree | 3c48bfbd9b00a765dea60ba12a3145370950800b /contrib/interface/xlate.ml | |
| parent | 701b613fd6f5e27cf69584171fb853cbf48f4530 (diff) | |
Ajout 'Print Scopes' et 'Bind Scope with classes'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4369 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index afa9226e1..a245a4b63 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1471,6 +1471,7 @@ let xlate_vernac = | PrintTables -> xlate_error "TODO: Print Tables" | PrintModuleType _ -> xlate_error "TODO: Print Module Type" | PrintModule _ -> xlate_error "TODO: Print Module" + | PrintScopes -> xlate_error "TODO: Print Scopes" | PrintScope _ -> xlate_error "TODO: Print Scope") | VernacBeginSection id -> CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id)) @@ -1618,6 +1619,8 @@ let xlate_vernac = | VernacDelimiters _ -> xlate_error "TODO: Delimiters" + | VernacBindScope _ -> xlate_error "TODO: Bind Scope" + | VernacNotation _ -> xlate_error "TODO: Notation" | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented" |