diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-12 11:22:53 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-10-12 11:22:53 +0200 |
commit | 6e49be2c03f11f412d17e41ca2e74232d12d915c (patch) | |
tree | e8a55b1349d84ba35856b5fd764ed4023a7f1d95 | |
parent | 6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff) | |
parent | 2bcae5b7a22019718973f65cafd271f735d3d85b (diff) |
Merge remote-tracking branch 'git/bug5123' into v8.5
-rw-r--r-- | proofs/proof.ml | 9 | ||||
-rw-r--r-- | proofs/proofview.ml | 36 | ||||
-rw-r--r-- | proofs/proofview.mli | 8 | ||||
-rw-r--r-- | test-suite/bugs/closed/5123.v | 33 |
4 files changed, 69 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} *) diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 000000000..bcde510ee --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,33 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. +Abort.
\ No newline at end of file |