Skip to content
Snippets Groups Projects

Fix refines_xchg_r

Closed Fix refines_xchg_r
NiklasM/reloc:fix-refines_xchg_r into master
Closed Niklas Mück requested to merge NiklasM/reloc:fix-refines_xchg_r into master
Compare
and
2 files
+ 9
− 9
Compare changes
  • Side-by-side
  • Inline
Files
2
theories/logic/proofmode/spec_tactics.v
+ 7
− 7
@@ -225,14 +225,14 @@ Qed.
Tactic Notation "tp_xchg" constr(j) :=
iStartProof;
eapply (tac_tp_store j);
[iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
|solve_ndisj || fail "tp_store: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
eapply (tac_tp_xchg j);
[iSolveTC || fail "tp_xchg: cannot eliminate modality in the goal"
|solve_ndisj || fail "tp_xchg: cannot prove 'nclose specN ⊆ ?'"
|iAssumptionCore || fail "tp_xchg: cannot find '" j " ' RHS"
|tp_bind_helper
|iSolveTC || fail "tp_store: cannot convert the argument to a value"
|iAssumptionCore || fail "tp_store: cannot find '? ↦ₛ ?'"
|simpl; reflexivity || fail "tp_store: this should not happen"
|iSolveTC || fail "tp_xchg: cannot convert the argument to a value"
|iAssumptionCore || fail "tp_xchg: cannot find '? ↦ₛ ?'"
|simpl; reflexivity || fail "tp_xchg: this should not happen"
|pm_reduce (* new goal *)].
(* *)