diff options
| -rw-r--r-- | proofs/proof.ml | 22 | ||||
| -rw-r--r-- | proofs/proofview.ml | 25 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 |
3 files changed, 33 insertions, 18 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 8dc9184b82..ca98af9772 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -322,15 +322,23 @@ let compact p = let run_tactic env tac pr = let sp = pr.proofview in - let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply env tac sp in - let shelf = - let sigma = Proofview.return tacticced_proofview in - let pre_shelf = pr.shelf@(List.rev (Evd.future_goals sigma))@to_shelve in - (* avoid already to count already solved goals as shelved. *) - List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf + let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = + Proofview.apply env tac sp + in + let sigma = Proofview.return tacticced_proofview in + (* Already solved goals are not to be counted as shelved. Nor are + they to be marked as unresolvable. *) + let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in + let retrieved = undef (List.rev (Evd.future_goals sigma)) in + let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_goal + tacticced_proofview + retrieved in let given_up = pr.given_up@give_up in - let proofview = Proofview.Unsafe.reset_future_goals tacticced_proofview in + let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) (*** Commands ***) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index ff0e57be2b..01bb41ad35 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -815,6 +815,19 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } + let mark_as_goal_evm evd content = + let info = Evd.find evd content in + let info = + { info with Evd.evar_source = match info.Evd.evar_source with + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + in + let info = Typeclasses.mark_unresolvable info in + Evd.add evd content info + + let mark_as_goal p gl = + { p with solution = mark_as_goal_evm p.solution gl } + end @@ -937,16 +950,6 @@ end module Refine = struct - let mark_as_goal evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = Typeclasses.mark_unresolvable info in - Evd.add evd content info - let typecheck_evar ev env sigma = let info = Evd.find sigma ev in let evdref = ref sigma in @@ -995,7 +998,7 @@ struct let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in (** Select the goals *) let comb = undefined sigma (CList.rev evs) in - let sigma = CList.fold_left mark_as_goal sigma comb in + let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >> Pv.set { solution = sigma; comb; } diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 7e755d23d6..eb54ba3ae5 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -392,6 +392,10 @@ module Unsafe : sig (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview + + (** Give an evar the status of a goal (changes its source location + and makes it unresolvable for type classes. *) + val mark_as_goal : proofview -> Evar.t -> proofview end (** {7 Notations} *) |