| [] -> assert false
| (g, t, k, tag) :: s ->
match init_pos g with (* TODO *)
- | [] | [ _ ] -> fail (lazy "too few goals to branch");
+ | [] | [ _ ] -> fail (lazy "too few goals to branch")
| loc :: loc_tl ->
([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
in
}
;;
+let ref_of_indtyinfo iti = iti.reference;;
+
let analyze_indty_tac ~what indtyref =
distribute_tac (fun status goal ->
let goalty = get_goalty status goal in