diff options
| author | herbelin | 2004-01-29 12:50:32 +0000 |
|---|---|---|
| committer | herbelin | 2004-01-29 12:50:32 +0000 |
| commit | 0d579625ec962e199b6b9bc153817080611e8016 (patch) | |
| tree | 80a9750b797fae16c7ba0532ff7da824fb014ca8 /contrib/interface | |
| parent | 6a4a791907af271b69b6709a54380e2f7f1b25a1 (diff) | |
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id := c"
de "Notation "'id'" := c"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5264 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 0e6fc29980..f19404e106 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1798,8 +1798,10 @@ let rec xlate_vernac = xlate_sort sort) in CT_ind_scheme (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi)) - | VernacSyntacticDefinition ((_,id), c, nopt) -> - CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt nopt) + | 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" | VernacRequire (impexp, spec, id::idl) -> let ct_impexp, ct_spec = get_require_flags impexp spec in CT_require (ct_impexp, ct_spec, |