From 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 22 Nov 2000 21:32:03 +0000 Subject: Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/metasyntax.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'toplevel/metasyntax.ml') 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, [])) -- cgit v1.2.3