X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fground.ml;fp=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fground.ml;h=91d85bc36443e1ac1d296abb486762cf14c69ca5;hb=f462726eaf4edb5852851ec5d265cdafe9d3a78d;hp=0e9f28c55bb0578b95f89f8e96957b508b26dd65;hpb=ffc3e681a82dc32269cc87407a95db6c922d3bfb;p=helm.git

diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml
index 0e9f28c55..91d85bc36 100644
--- a/matita/components/binaries/matex/ground.ml
+++ b/matita/components/binaries/matex/ground.ml
@@ -48,6 +48,10 @@ let rec foldi_left mapi i a = function
    | []       -> a
    | hd :: tl -> foldi_left mapi (succ i) (mapi i a hd) tl
 
+let rec rev_mapi mapi i l =
+   let map i a hd = mapi i hd :: a in
+   foldi_left map i [] l
+
 let rec rev_map_append map l r = match l with
    | []       -> r
    | hd :: tl -> rev_map_append map tl (map hd :: r)