+let name_of_obj = function
+ | Theorem (_,n,_,_,_) | Record (_,n,_,_)
+ | Inductive (_,(n,_,_,_)::_) -> n
+ | _ -> (* empty inductive block *) assert false
+;;
+
+let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
+
+let map_pattern f = function
+ | Pattern (s,h,vl) -> Pattern (s,h,List.map (map_variable f) vl)
+ | p -> p
+;;
+
+let map f = function
+ | AttributedTerm (a,u) -> AttributedTerm (a,f u)
+ | Appl tl -> Appl (List.map f tl)
+ | Binder (k,n,body) -> Binder (k,map_variable f n,f body)
+ | Case (t,ity,oty,pl) ->
+ let pl' = List.map (fun (p,u) -> map_pattern f p, f u) pl in
+ Case (f t,ity,HExtlib.map_option f oty,pl')
+ | Cast (u,v) -> Cast (f u,f v)
+ | LetIn (n,u,v) -> LetIn (n,f u,f v)
+ | LetRec (ik,l,t) ->
+ let l' = List.map (fun (vl,v,u,n) ->
+ (List.map (map_variable f) vl,
+ map_variable f v,
+ f u,
+ n)) l
+ in LetRec (ik,l',f t)
+ | t -> t
+;;
+