From 0141ad09a89784de0d8b3d02f7574e2a7f29bd7e Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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 +++++++
 1 file changed, 7 insertions(+)

(limited to 'toplevel/metasyntax.ml')

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
-- 
cgit v1.2.3