- (* choices is a list of pairs proof and goallist *)
- let choices =
- (search_theorems_in_context ~status:(proof,goal))@
- (TacticChaser.searchTheorems mqi_handle ~status:(proof,goal))
- in
- let rec try_choices = function
- [] -> raise NotApplicableTheorem
- | (proof,goallist)::tl ->
+ (* let us verify that the metavariable is still an open goal --
+ it could have been closed by closing other goals -- and that
+ it is of sort Prop *)
+ let _,metasenv,_,_ = proof in
+ let meta_inf =
+ (try
+ let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
+ Some (ey, ty)
+ with _ -> None) in
+ match meta_inf with
+ Some (ey, ty) ->
+ prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
+ prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
+ (*
+ let time1 = Unix.gettimeofday() in
+ let _, all_paths = NewConstraints.prefixes 5 ty in
+ let time2 = Unix.gettimeofday() in
+ prerr_endline
+ (Printf.sprintf "TEMPO DI CALCOLO = %1.3f" (time2 -. time1) );
+ prerr_endline
+ ("ALL PATHS: n = " ^ string_of_int
+ (List.length all_paths));
+ prerr_endline (NewConstraints.pp_prefixes all_paths);
+ *)
+ (* if the goal does not have a sort Prop we return the
+ current proof and a list containing the goal *)
+ let ty_sort = CicTypeChecker.type_of_aux' metasenv ey ty in
+ if CicReduction.are_convertible
+ ey (Cic.Sort Cic.Prop) ty_sort then
+ (* sort Prop *)
+ (* choices is a list of pairs proof and goallist *)
+ let choices =
+ (search_theorems_in_context (proof,goal))@
+ (TacticChaser.searchTheorems mqi_handle (proof,goal))
+ in
+ let rec try_choices = function
+ [] -> raise NotApplicableTheorem
+ | (proof,goallist)::tl ->