From 3dac1f2b8c6afcd955db1f7a289cf377abc1af44 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 22 Nov 2003 13:42:04 +0000
Subject: Traitement plus clair, notamment pour Locate, de quand quoter les
 composantes de notations + contournement du fait que Lexer arrive apres
 Symbol

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4972 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'toplevel/metasyntax.mli')

diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 74b199ed7..8f6b49d0e 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -59,3 +59,5 @@ val merge_modifiers : Gramext.g_assoc option -> int option ->
 
 val interp_infix_modifiers : syntax_modifier list ->
   Gramext.g_assoc option * precedence option * bool * string located option
+
+val standardise_locatable_notation : string -> string
-- 
cgit v1.2.3