+ let order_body_menv term body_metasenv =
+ let rec purge_lambdas = function
+ | Cic.Lambda (_,_,t) -> purge_lambdas t
+ | t -> t
+ in
+ let skip_appl = function | Cic.Appl l -> List.tl l | _ -> assert false in
+ let metas_that_saturate l =
+ List.fold_left
+ (fun (acc,n) t ->
+ let metas = CicUtil.metas_of_term t in
+ let metas = List.map fst metas in
+ let metas =
+ List.filter
+ (fun i -> List.for_all (fun (j,_) -> j<>i) acc)
+ metas
+ in
+ let metas = List.map (fun i -> i,n) metas in
+ metas @ acc, n+1)
+ ([],0) l
+ in
+ let l_c2 = skip_appl (purge_lambdas term) in
+ let l_c1 =
+ match HExtlib.list_last l_c2 with
+ | Cic.Appl l -> List.tl l
+ | _ -> assert false
+ in
+ (* i should cut off the laet elem of l_c2 *)
+ let meta2no = fst (metas_that_saturate (l_c1 @ l_c2)) in
+ List.sort
+ (fun (i,ctx1,ty1) (j,ctx1,ty1) ->
+ try List.assoc i meta2no - List.assoc j meta2no
+ with Not_found -> assert false)
+ body_metasenv
+ in
+ let namer l n =
+ let l = List.map (function Cic.Name s -> s | _ -> "A") l in
+ let l = List.fold_left
+ (fun acc s ->
+ let rec add' s =
+ if List.exists ((=) s) acc then add' (s^"'") else s
+ in
+ acc@[add' s])
+ [] l
+ in
+ let l = List.rev l in
+ Cic.Name (List.nth l (n-1))
+ in