diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-15 11:49:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-15 11:49:01 +0000 |
| commit | 54c62085a4c08273fb3967d91250df9516d3bfba (patch) | |
| tree | 9dbf99c274bacf11494941ed9291ffa30c387e64 /contrib | |
| parent | 05480018d2e8826b15a808fb0d70a7b293109cc2 (diff) | |
Ajout Print Implicit avec depliage du type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/xlate.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 6b4b82e39..5e0bc4d9f 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1474,7 +1474,8 @@ let xlate_vernac = | PrintScopes -> xlate_error "TODO: Print Scopes" | PrintScope _ -> xlate_error "TODO: Print Scope" | PrintVisibility _ -> xlate_error "TODO: Print Visibility" - | PrintAbout _ -> xlate_error "TODO: Print About") + | PrintAbout _ -> xlate_error "TODO: Print About" + | _ -> xlate_error "TODO: Print") | VernacBeginSection id -> CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id)) | VernacEndSegment id -> CT_section_end (xlate_ident id) |