-(*
-let apply_to_goal env theorems active (depth, goals) =
- let _ =
- debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals)))
- in
- let metasenv, context, ugraph = env in
- let goal = List.hd goals in
- let proof, metas, term = goal in
-(* debug_print *)
-(* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *)
- let newmeta = CicMkImplicit.new_meta metasenv [] in
- let metasenv = (newmeta, context, term)::metasenv @ metas in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let status =
- ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta)
- in
- let rec aux = function
- | [] -> false, [] (* goals *) (* None *)
- | (theorem, thmty, _)::tl ->
- try
- let subst_in, (newproof, newgoals) =
- PrimitiveTactics.apply_tac_verbose ~term:theorem status
- in
- if newgoals = [] then
- let _, _, p, _ = newproof in
- let newp =
- let rec repl = function
- | Inference.ProofGoalBlock (_, gp) ->
- Inference.ProofGoalBlock (Inference.BasicProof p, gp)
- | Inference.NoProof -> Inference.BasicProof p
- | Inference.BasicProof _ -> Inference.BasicProof p
- | Inference.SubProof (t, i, p2) ->
- Inference.SubProof (t, i, repl p2)
- | _ -> assert false
- in
- repl proof
- in
- true, [[newp, metas, term]] (* Some newp *)
- else if List.length newgoals = 1 then
- let _, menv, p, _ = newproof in
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let goals =
- List.map
- (fun i ->
- let _, _, ty = CicUtil.lookup_meta i menv in
- let proof =
- Inference.SubProof
- (p, i, Inference.BasicProof (Cic.Meta (i, irl)))
- in (proof, menv, ty))
- newgoals
- in
- let res, others = aux tl in
- if res then (true, others) else (false, goals::others)
- else
- aux tl
- with ProofEngineTypes.Fail msg ->
- (* debug_print ("FAIL!!:" ^ msg); *)
- aux tl
- in
- let r, l =
- if Inference.term_is_equality term then
- let rec appleq = function
- | [] -> false, []
- | (Positive, equality)::tl ->
- let ok, _, newproof = apply_equality_to_goal env equality goal in
- if ok then true, [(depth, [newproof, metas, term])] else appleq tl
- | _::tl -> appleq tl
- in
- let al, _ = active in
- appleq al
- else
- false, []
- in
- if r = true then r, l else
- let r, l = aux theorems in
- if r = true then
- r, List.map (fun l -> (depth+1, l)) l
- else
- r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l)
-;;
-*)
-