From 0141ad09a89784de0d8b3d02f7574e2a7f29bd7e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 10 Sep 2003 14:28:07 +0000
Subject: Traduction de Distfix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4344 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml  | 7 +++++++
 toplevel/metasyntax.mli | 3 +++
 2 files changed, 10 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3d11b2412e..2a5fd697c9 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -888,6 +888,13 @@ let rec rename x vars n = function
   | WhiteSpace _::l ->
       rename x vars n l
 
+let translate_distfix assoc df r = 
+  let (vars,l) = rename "x" [] 1 (split df) in
+  let df = String.concat " " l in
+  let a = mkAppC (mkRefC r, vars) in
+  let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
+  (assoc,df,a)
+
 let add_distfix local assoc n df r sc =
   (* "x" cannot clash since r is globalized (included section vars) *)
   let (vars,l) = rename "x" [] 1 (split df) in
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index aae9229125..31b8e046d0 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -35,6 +35,9 @@ val add_infix : locality_flag ->
 val add_distfix : locality_flag ->
   grammar_associativity -> precedence -> string -> reference
     -> scope_name option -> unit
+val translate_distfix : grammar_associativity -> string -> reference ->
+  Gramext.g_assoc * string * constr_expr
+
 val add_delimiters : scope_name -> string -> unit
 
 val add_notation : locality_flag -> constr_expr
-- 
cgit v1.2.3