Traduction de Distfix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4344 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3d11b2412..2a5fd697c 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