exception NoOtherChoices;;
-let is_in_metasenv goal metasenv =
- try
- let (_, ey ,ty) =
- CicUtil.lookup_meta goal metasenv in
- true
- with CicUtil.Meta_not_found _ -> false
-
let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
universe
=
let _,metasenv,p,_ = proof in
(* first of all we check if the goal has been already
inspected *)
- assert (is_in_metasenv goal metasenv);
+ assert (CicUtil.exists_meta goal metasenv);
let exitus =
try Hashtbl.find inspected_goals ty
with Not_found -> NotYetInspected in
| [] -> []
| (subst,(proof, goals, sign))::tl ->
let _,metasenv,_,_ = proof in
- let is_in_metasenv (goal, _) =
- try
- let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
- true
- with CicUtil.Meta_not_found _ -> false
+ let goals'=
+ List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
in
- let goals'= List.filter is_in_metasenv goals in
auto_new_aux dbd
width already_seen_goals universe ((subst,(proof, goals', sign))::tl)