aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/proofview.ml37
-rw-r--r--engine/proofview.mli8
-rw-r--r--proofs/proof.ml9
-rw-r--r--test-suite/bugs/closed/5123.v33
-rw-r--r--test-suite/success/Typeclasses.v2
-rw-r--r--theories/FSets/FSetDecide.v19
-rw-r--r--theories/MSets/MSetDecide.v19
7 files changed, 82 insertions, 45 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index f2f400515..85a52fdca 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -685,6 +685,21 @@ 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 = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
+ | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
+ | Some () -> info
+ in
+ Evd.add evd content info
+
let with_shelf tac =
let open Proof in
Pv.get >>= fun pv ->
@@ -697,8 +712,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]].*)
@@ -945,20 +963,13 @@ module Unsafe = struct
{ p with solution = Evd.reset_future_goals p.solution }
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 = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
- | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
- | Some () -> info
- in
- Evd.add evd content info
+ mark_in_evm ~goal:true evd content
let advance = advance
+ let mark_as_unresolvable p gl =
+ { p with solution = mark_in_evm ~goal:false p.solution gl }
+
let typeclass_resolvable = typeclass_resolvable
end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index fae75f825..725445251 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -326,8 +326,9 @@ val unshelve : Goal.goal list -> proofview -> proofview
(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
-(** [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]
@@ -434,6 +435,9 @@ module Unsafe : sig
and makes it unresolvable for type classes. *)
val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+ (** Make an evar unresolvable for type classes. *)
+ val mark_as_unresolvable : proofview -> Evar.t -> proofview
+
(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
the current avatar of [g] (for instance [g] was changed by [clear]
into [g']). It returns [None] if [g] has been (partially)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5fe29653d..5c963d53e 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -351,7 +351,14 @@ let run_tactic env tac pr =
Proofview.apply env tac sp
in
let sigma = Proofview.return proofview in
- let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in
+ let to_shelve = undef sigma to_shelve in
+ let shelf = (undef sigma pr.shelf)@retrieved@to_shelve 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/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
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index dfa438d90..3eaa04144 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -5,7 +5,7 @@ Record Equ (A : Type) (R : A -> A -> Prop).
Definition equiv {A} R (e : Equ A R) := R.
Record Refl (A : Type) (R : A -> A -> Prop).
Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
-Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo.
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo.
Variable R : nat -> nat -> Prop.
Lemma bas : Equ nat R.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index ad067eb3d..1db6a71e8 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -357,17 +357,8 @@ the above form:
| _ => idtac
end.
- (** [if t then t1 else t2] executes [t] and, if it does not
- fail, then [t1] will be applied to all subgoals
- produced. If [t] fails, then [t2] is executed. *)
- Tactic Notation
- "if" tactic(t)
- "then" tactic(t1)
- "else" tactic(t2) :=
- first [ t; first [ t1 | fail 2 ] | t2 ].
-
Ltac abstract_term t :=
- if (is_var t) then fail "no need to abstract a variable"
+ tryif (is_var t) then fail "no need to abstract a variable"
else (let x := fresh "x" in set (x := t) in *; try clearbody x).
Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
repeat (
match goal with
| H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
- if (change T with E.t in H) then fail
- else if (change T with t in H) then fail
+ tryif (change T with E.t in H) then fail
+ else tryif (change T with t in H) then fail
else clear H
| H : ?P |- _ =>
- if prop (FSet_Prop P) holds by
+ tryif prop (FSet_Prop P) holds by
(auto 100 with FSet_Prop)
then fail
else clear H
@@ -747,7 +738,7 @@ the above form:
| H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
contradict H; fsetdec_body
| H: ?P -> False |- ?Q -> False =>
- if prop (FSet_elt_Prop P) holds by
+ tryif prop (FSet_elt_Prop P) holds by
(auto 100 with FSet_Prop)
then (contradict H; fsetdec_body)
else fsetdec_body
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791b..9c622fd78 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -357,17 +357,8 @@ the above form:
| _ => idtac
end.
- (** [if t then t1 else t2] executes [t] and, if it does not
- fail, then [t1] will be applied to all subgoals
- produced. If [t] fails, then [t2] is executed. *)
- Tactic Notation
- "if" tactic(t)
- "then" tactic(t1)
- "else" tactic(t2) :=
- first [ t; first [ t1 | fail 2 ] | t2 ].
-
Ltac abstract_term t :=
- if (is_var t) then fail "no need to abstract a variable"
+ tryif (is_var t) then fail "no need to abstract a variable"
else (let x := fresh "x" in set (x := t) in *; try clearbody x).
Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
repeat (
match goal with
| H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
- if (change T with E.t in H) then fail
- else if (change T with t in H) then fail
+ tryif (change T with E.t in H) then fail
+ else tryif (change T with t in H) then fail
else clear H
| H : ?P |- _ =>
- if prop (MSet_Prop P) holds by
+ tryif prop (MSet_Prop P) holds by
(auto 100 with MSet_Prop)
then fail
else clear H
@@ -747,7 +738,7 @@ the above form:
| H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
contradict H; fsetdec_body
| H: ?P -> False |- ?Q -> False =>
- if prop (MSet_elt_Prop P) holds by
+ tryif prop (MSet_elt_Prop P) holds by
(auto 100 with MSet_Prop)
then (contradict H; fsetdec_body)
else fsetdec_body
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 09:48:13 +0000