let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
- [] -> []
+ | [] -> []
| hd::tl ->
- let res =
- try
- let (subst,(proof, goal_list)) =
- PT.apply_tac_verbose ~term:(C.Rel n) status in
- (*
- let goal_list =
- List.stable_sort (compare_goal_list proof) goal_list in
- *)
- Some (subst,(proof, goal_list))
- with
- PET.Fail _ -> None in
- (match res with
- Some res -> res::(find (n+1) tl)
- | None -> find (n+1) tl)
+ let res =
+ (* we should check that the hypothesys has not been cleared *)
+ if List.nth context (n-1) = None then
+ None
+ else
+ try
+ let (subst,(proof, goal_list)) =
+ PT.apply_tac_verbose ~term:(C.Rel n) status
+ in
+ (*
+ let goal_list =
+ List.stable_sort (compare_goal_list proof) goal_list in
+ *)
+ Some (subst,(proof, goal_list))
+ with
+ PET.Fail _ -> None
+ in
+ (match res with
+ | Some res -> res::(find (n+1) tl)
+ | None -> find (n+1) tl)
in
try
find 1 context
- with Failure s ->
- []
+ with Failure s -> []
;;
let (_, ey ,ty) =
CicUtil.lookup_meta goal metasenv in
true
- with _ -> false
+ with CicUtil.Meta_not_found _ -> false
let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
universe
end
and auto_new dbd width already_seen_goals universe = function
- [] -> []
+ | [] -> []
| (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 _ -> false in
+ try
+ let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
+ true
+ with CicUtil.Meta_not_found _ -> false
+ in
let goals'= List.filter is_in_metasenv goals in
- auto_new_aux dbd width already_seen_goals universe
- ((subst,(proof, goals', sign))::tl)
+ auto_new_aux dbd
+ width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
and auto_new_aux dbd width already_seen_goals universe = function
- [] -> []
+ | [] -> []
| (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
| (subst,(proof, (goal,0)::_, _))::tl ->
auto_new dbd width already_seen_goals universe tl