diff options
author | 2016-10-12 11:22:53 +0200 | |
---|---|---|
committer | 2016-10-12 11:22:53 +0200 | |
commit | 6e49be2c03f11f412d17e41ca2e74232d12d915c (patch) | |
tree | e8a55b1349d84ba35856b5fd764ed4023a7f1d95 /proofs | |
parent | 6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff) | |
parent | 2bcae5b7a22019718973f65cafd271f735d3d85b (diff) |
Merge remote-tracking branch 'git/bug5123' into v8.5
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/proof.ml | 9 | ||||
-rw-r--r-- | proofs/proofview.ml | 36 | ||||
-rw-r--r-- | proofs/proofview.mli | 8 |
3 files changed, 36 insertions, 17 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 0489305aa..1f094b339 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -343,13 +343,20 @@ let run_tactic env tac pr = 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 to_shelve = undef to_shelve in + let shelf = (undef pr.shelf)@retrieved@to_shelve in let proofview = List.fold_left Proofview.Unsafe.mark_as_goal tacticced_proofview retrieved in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_unresolvable + proofview + to_shelve + in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in { pr with proofview ; shelf ; given_up },(status,info_trace) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 91905be62..2fc404235 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -642,6 +642,18 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } +let mark_in_evm ~goal evd content = + let info = Evd.find evd content in + let info = + if goal then + { 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 } + else info + in + let info = Typeclasses.mark_unresolvable info in + Evd.add evd content info + let with_shelf tac = let open Proof in Pv.get >>= fun pv -> @@ -654,8 +666,11 @@ let with_shelf tac = let fgoals = Evd.future_goals solution in let pgoal = Evd.principal_future_goal solution in let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) + (* Ensure we mark and return only unsolved goals *) + let gls' = undefined sigma (CList.rev_append gls' gls) in + let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let npv = { npv with shelf; solution = sigma } in + Pv.set npv >> tclUNIT (gls', ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the interval [[0,m-1]].*) @@ -893,18 +908,11 @@ 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 } + { p with solution = mark_in_evm ~goal:true p.solution gl } + + let mark_as_unresolvable p gl = + { p with solution = mark_in_evm ~goal:false p.solution gl } end @@ -1128,7 +1136,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 Unsafe.mark_as_goal_evm sigma comb in + let sigma = CList.fold_left (mark_in_evm ~goal:true) sigma comb in let open Proof in InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 1a367f4ea..c8d96fe79 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -303,8 +303,9 @@ val guard_no_unifiable : unit tactic goals of p *) val unshelve : Goal.goal list -> proofview -> proofview -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) +(** [with_shelf tac] executes [tac] and returns its result together with + the set of goals shelved by [tac]. The current shelf is unchanged + and the returned list contains only unsolved goals. *) val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] @@ -407,6 +408,9 @@ module Unsafe : sig (** 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 + + (** Make an evar unresolvable for type classes. *) + val mark_as_unresolvable : proofview -> Evar.t -> proofview end (** {7 Notations} *) |