+let initial_status ty metasenv =
+ let rec aux max = function
+ | [] -> max + 1
+ | (idx, _, _) :: tl ->
+ if idx > max then
+ aux idx tl
+ else
+ aux max tl
+ in
+ let newmeta_idx = aux 0 metasenv in
+ let proof =
+ None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty
+ in
+ (proof, newmeta_idx)
+