- improved support for case

[helm.git] / matita / components / binaries / matex / ground.ml

diff --git a/matita/components/binaries/matex/ground.ml b/matita/components/binaries/matex/ground.ml
index 0e9f28c55bb0578b95f89f8e96957b508b26dd65..91d85bc36443e1ac1d296abb486762cf14c69ca5 100644 (file)
--- 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)