+let saturate_term (id_to_eq, maxmeta) metasenv subst context term =
+ let maxmeta = max maxmeta (CicMkImplicit.new_meta metasenv subst) in
+ let head, metasenv, args, newmeta =
+ TermUtil.saturate_term maxmeta metasenv context term 0
+ in
+ (id_to_eq, newmeta), head, metasenv, args
+;;
+
+let push_maxmeta (id_to_eq, maxmeta) m = id_to_eq, max maxmeta m ;;
+let filter_metasenv_gt_maxmeta (_,maxmeta) =
+ List.filter (fun (j,_,_) -> j >= maxmeta)
+;;
+let maxmeta = snd;;