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 /toplevel/metasyntax.ml | |
| 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 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 538c7563a3..a50339c6e9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1111,14 +1111,6 @@ let add_notation local c dfmod mv8 sc = | Some (df,modifiers) -> let toks = split_notation_string df in match toks with - | [String x] when is_quoted_ident x - (* This is an ident that can be qualified: a syntactic definition *) - & (modifiers = [] or modifiers = [SetOnlyParsing]) -> - (* Means a Syntactic Definition *) - let ident = id_of_string (unquote_notation_token x) in - let c = snd (interp_aconstr [] [] c) in - let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in - Syntax_def.declare_syntactic_definition local ident onlyparse c | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) -> (* This is a ident to be declared as a rule *) add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc toks |