diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 22:49:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-30 22:49:55 +0000 |
| commit | 45f5a9e88a35412c49703c95dbca6c38b9340e11 (patch) | |
| tree | 7800ce50c5de2da1c519a08b43c3de55329562b6 | |
| parent | 7944955b892f0ffa70ecf92f83b372cddc5b867b (diff) | |
Suite commit 10730: MAJ xlate.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10732 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index aa7a50dce..0e5798210 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1982,10 +1982,10 @@ let rec xlate_vernac = CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme" - | VernacSyntacticDefinition (id, c, false, _) -> + | VernacSyntacticDefinition (id, ([],c), false, _) -> CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None) - | VernacSyntacticDefinition (id, c, true, _) -> - xlate_error "TODO: Local abbreviations" + | VernacSyntacticDefinition (id, _, true, _) -> + xlate_error"TODO: Local abbreviations and abbreviations with parameters" (* Modules and Module Types *) | VernacInclude (_) -> xlate_error "TODO : Include " | VernacDeclareModuleType((_, id), bl, mty_o) -> |