diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
| commit | 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 (patch) | |
| tree | 3a2c73669cb40011c2e62a11d3364d39f74040ba /toplevel/metasyntax.ml | |
| parent | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (diff) | |
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d1bada0c2..eb7543f3d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -219,7 +219,7 @@ let add_infix assoc n inf pr = [< 'sTR"Associativity Precedence must be 6,7,8 or 9." >]; (* check the grammar entry *) let prefast = Astterm.ast_of_qualid dummy_loc pr in - let prefname = (Names.string_of_path pr)^"_infix" in + let prefname = (Names.string_of_qualid pr)^"_infix" in let gram_rule = gram_infix assoc n (split inf) prefname prefast in (* check the syntax entry *) let syntax_rule = infix_syntax_entry assoc n inf prefname prefast in @@ -267,7 +267,7 @@ let distfix assoc n sl fname astf = } let add_distfix a n df f = - let fname = (Names.string_of_path f)^"_distfix" in + let fname = (Names.string_of_qualid f)^"_distfix" in let astf = Astterm.ast_of_qualid dummy_loc f in Lib.add_anonymous_leaf (inInfix(distfix a n (split df) fname astf, [])) |