From 3928384774dd1e009b95420f063addab24bff639 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 Feb 2020 13:50:30 +0100
Subject: [PATCH] no longer reftest old Coq 8.9
---
Makefile.coq.local | 2 +-
tests/atomic.ref | 4 -
tests/atomic.v | 1 -
tests/heap_lang.ref | 2 -
tests/heap_lang.v | 1 -
tests/list_reverse.8.9.ref | 33 -------
tests/proofmode.ref | 172 ------------------------------------
tests/proofmode.v | 1 -
tests/proofmode_iris.ref | 12 ---
tests/proofmode_iris.v | 1 -
tests/proofmode_monpred.ref | 3 -
tests/proofmode_monpred.v | 1 -
tests/proofmode_siprop.v | 1 -
13 files changed, 1 insertion(+), 233 deletions(-)
delete mode 100644 tests/list_reverse.8.9.ref
diff --git a/Makefile.coq.local b/Makefile.coq.local
index fe6320aa2..9ceafe4c7 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -9,7 +9,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY: test
COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8)\b" -q && echo 1)
+COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
tests/.coqdeps.d: $(TESTFILES)
diff --git a/tests/atomic.ref b/tests/atomic.ref
index e1099c9c8..ba5c5ad60 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -15,12 +15,8 @@
"non_laterable"
: string
The command has indeed failed with message:
-Ltac call to "iAuIntro" failed.
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
The command has indeed failed with message:
-In nested Ltac calls to "awp_apply (open_constr)",
-"<ssreflect_plugin::ssrtclseq@0> wp_apply_core lem fun H => iApplyHyp H ; last iAuIntro" and
-"iAuIntro", last call failed.
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"printing"
: string
diff --git a/tests/atomic.v b/tests/atomic.v
index afc6e55bd..125a261c1 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -2,7 +2,6 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Set Default Proof Using "Type".
Section tests.
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index ac83b6d40..8d19418d3 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -75,7 +75,6 @@
"wp_nonclosed_value"
: string
The command has indeed failed with message:
-Ltac call to "wp_pure (open_constr)" failed.
Tactic failure: wp_pure: cannot find ?y in (Var "x") or
?y is not a redex.
1 subgoal
@@ -175,6 +174,5 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
"not_cmpxchg"
: string
The command has indeed failed with message:
-Ltac call to "wp_cmpxchg_suc" failed.
Tactic failure: wp_cmpxchg_suc: cannot find 'CmpXchg' in
(#() #()).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 8cc493fd7..942b4bb79 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Import lang adequacy proofmode notation.
(* Import lang *again*. This used to break notation. *)
From iris.heap_lang Require Import lang.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Set Default Proof Using "Type".
Section tests.
diff --git a/tests/list_reverse.8.9.ref b/tests/list_reverse.8.9.ref
deleted file mode 100644
index 2c8d90077..000000000
--- a/tests/list_reverse.8.9.ref
+++ /dev/null
@@ -1,33 +0,0 @@
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- hd, acc : val
- xs, ys : list val
- Φ : val → iPropI Σ
- ============================
- "Hxs" : is_list hd xs
- "Hys" : is_list acc ys
- "HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
- --------------------------------------∗
- WP (rev hd) acc [{ v, Φ v }]
-
-1 subgoal
-
- Σ : gFunctors
- heapG0 : heapG Σ
- acc : val
- ys : list val
- Φ : val → iPropI Σ
- ============================
- "Hys" : is_list acc ys
- "HΦ" : ∀ w : val, is_list w ys -∗ Φ w
- --------------------------------------∗
- WP match: InjLV #() with
- InjL <> => acc
- | InjR "l" =>
- let: "tmp1" := Fst ! "l" in
- let: "tmp2" := Snd ! "l" in
- "l" <- ("tmp1", acc);; (rev "tmp2") (InjLV #())
- end [{ v, Φ v }]
-
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index be894c20a..e45044a82 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -78,50 +78,21 @@
Q
The command has indeed failed with message:
-Ltac call to "done" failed.
No applicable tactic.
The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HQ" not found.
The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr) as #",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)" and
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-last call failed.
Tactic failure: iSpecialize: Q not persistent.
"test_iAssert_intuitionistic"
: string
The command has indeed failed with message:
-In nested Ltac calls to "<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first done",
-"<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first done",
-"iAssert (open_constr) with (constr) as (constr)",
-"iAssertCore (open_constr) with (constr) as (constr) (tactic3)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
Tactic failure: iSpecialize: (|==> P)%I not persistent.
The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
P.
The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I with P.
"test_iNext_plus_3"
: string
@@ -185,9 +156,6 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌠→ P -∗ False)%I wi
"test_iSimpl_in4"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iSimpl in (constr)",
-"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
-last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
"test_iFrame_later_1"
: string
@@ -210,9 +178,6 @@ Tactic failure: iEval: %: unsupported selection pattern.
â–· emp
The command has indeed failed with message:
-In nested Ltac calls to "iFrame (constr)",
-"<iris.proofmode.ltac_tactics.iFrame_go>" and
-"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
Tactic failure: iFrame: cannot frame Q.
"test_and_sep_affine_bi"
: string
@@ -496,115 +461,71 @@ Tactic failure: iFrame: cannot frame Q.
"iStopProof_not_proofmode"
: string
The command has indeed failed with message:
-Ltac call to "iStopProof" failed.
Tactic failure: iStopProof: proofmode not started.
"iAlways_spatial_non_empty"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iAlways", "iModIntro" and
-"iModIntro (uconstr)", last call failed.
Tactic failure: iModIntro: spatial context is non-empty.
"iDestruct_bad_name"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic3)" and
-"iDestructCore (open_constr) as (constr) (tactic3)", last call failed.
Tactic failure: iDestruct: "HQ" not found.
"iIntros_dup_name"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
-"iIntro (constr)", last call failed.
Tactic failure: iIntro: "HP" not fresh.
The command has indeed failed with message:
-In nested Ltac calls to "iIntros ( (intropattern) )",
-"iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used.
"iSplitL_one_of_many"
: string
The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
"iSplitR_one_of_many"
: string
The command has indeed failed with message:
-Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
The command has indeed failed with message:
-Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
"iSplitL_non_splittable"
: string
The command has indeed failed with message:
-Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: P not a separating conjunction.
"iSplitR_non_splittable"
: string
The command has indeed failed with message:
-Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: P not a separating conjunction.
"iCombine_fail"
: string
The command has indeed failed with message:
-Ltac call to "iCombine (constr) as (constr)" failed.
Tactic failure: iCombine: hypotheses ["HP3"] not found.
"iSpecialize_bad_name1_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
Tactic failure: iSpecialize: "H" not found.
"iSpecialize_bad_name2_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
Tactic failure: iSpecialize: "H" not found.
"iExact_fail"
: string
The command has indeed failed with message:
-Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" not found.
The command has indeed failed with message:
-Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
-Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HP"
not absorbing and the remaining hypotheses not affine.
"iClear_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HP" not found.
The command has indeed failed with message:
-In nested Ltac calls to "iClear (constr)",
-"<iris.proofmode.ltac_tactics.iClear_go>" and
-"<iris.proofmode.ltac_tactics.iClearHyp>", last call failed.
Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
"iSpecializeArgs_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iSpecialize (open_constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializeArgs (constr) (open_constr)",
-"<iris.proofmode.ltac_tactics.iSpecializeArgs_go>" and
-"notypeclasses refine (uconstr)", last call failed.
In environment
PROP : sbi
P : PROP
@@ -612,173 +533,80 @@ The term "true" has type "bool" while it is expected to have type "nat".
"iStartProof_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iStartProof" and "iStartProof", last call failed.
Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (open_constr) as (tactic3)" and
-"iIntoEmpValid", last call failed.
Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
-fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
-"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
-"iRename (constr) into (constr)", last call failed.
Tactic failure: iRename: "H" not fresh.
"iPoseProof_not_found_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)" and
-"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProof_not_found_fail2"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
-fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
-fun Htmp =>
- lazymatch lem with
- | {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
- {| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
- | _ => idtac
- end), "iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) as (constr)",
-"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
-"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
-failed.
Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
"iPoseProofCoreHyp_not_found_fail"
: string
The command has indeed failed with message:
-Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProofCoreHyp_not_fresh_fail"
: string
The command has indeed failed with message:
-Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "H1" not fresh.
"iRevert_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iRevert (constr)", "iElaborateSelPat" and
-"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "H" not found.
"iDestruct_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"tac" (bound to fun H => iDestructHyp H as pat),
-"iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>", last call failed.
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
-In nested Ltac calls to "iDestruct (open_constr) as (constr)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"iDestructCore (open_constr) as (constr) (tactic3)",
-"tac" (bound to fun H => iDestructHyp H as pat),
-"iDestructHyp (constr) as (constr)",
-"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
-"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
"iOrDestruct_fail"
: string
The command has indeed failed with message:
-Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
The command has indeed failed with message:
-Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
"iApply_fail"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
-failed.
Tactic failure: iApply: cannot apply P.
"iApply_fail_not_affine_1"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
-failed.
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.
"iApply_fail_not_affine_2"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iApply (open_constr)",
-"iPoseProofCore (open_constr) as (constr) (tactic3)",
-"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
-failed.
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.
"iRevert_wrong_var"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) )" and
-"iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k1 not in scope.
The command has indeed failed with message:
-In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
-"iLöbRevert (constr) with (tactic3)",
-"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go",
-"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
-"∗" with tac), "iRevertIntros (constr) with (tactic3)",
-"iRevertIntros_go", "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as
-IH), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
-"iRevertIntros ( (ident) ) (constr) with (tactic3)",
-"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go",
-"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
-"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
-"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k1 not in scope.
"iRevert_dup_var"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) (ident) )",
-"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k not in scope.
"iRevert_dep_var_coq"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) )", "iForallRevert (ident)" and
-"revert (ne_var_list)", last call failed.
k is used in hypothesis Hk.
"iRevert_dep_var"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iRevert ( (ident) )" and
-"iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k is used in hypothesis "Hk".
"iLöb_no_sbi"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iLöb as (constr)",
-"iLöbRevert (constr) with (tactic3)",
-"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go",
-"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
-"∗" with tac), "iRevertIntros (constr) with (tactic3)",
-"iRevertIntros_go", "tac" (bound to iLöbCore as IH),
-"tac" (bound to iLöbCore as IH) and "iLöbCore as (constr)", last call failed.
Tactic failure: iLöb: not a step-indexed BI entailment.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index fc1e7df41..93876587b 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,4 @@
From iris.proofmode Require Import tactics intro_patterns.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Set Default Proof Using "Type".
Section tests.
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 6ebe13d84..9cbbce1b7 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -110,22 +110,10 @@
"test_iInv_12"
: string
The command has indeed failed with message:
-In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic3)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
-failed.
Tactic failure: iInv: selector 34 is not of the right type .
The command has indeed failed with message:
-In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic3)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
-failed.
Tactic failure: iInv: invariant nroot not found.
The command has indeed failed with message:
-In nested Ltac calls to "iInv (constr) as (constr)",
-"iInvCore (constr) in (tactic3)" and
-"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
-failed.
Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
: string
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 39fabcd8d..3392c95df 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,7 +1,6 @@
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Section base_logic_tests.
Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.ref b/tests/proofmode_monpred.ref
index 72d54d672..973c967d9 100644
--- a/tests/proofmode_monpred.ref
+++ b/tests/proofmode_monpred.ref
@@ -58,9 +58,6 @@
∀ _ : (), ∃ _ : (), emp
The command has indeed failed with message:
-In nested Ltac calls to "iFrame (constr)",
-"<iris.proofmode.ltac_tactics.iFrame_go>" and
-"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
Tactic failure: iFrame: cannot frame (P i).
1 subgoal
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 268ffa905..a1b445dbb 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,5 @@
From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
Section tests.
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index 34a032198..61d894ea4 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,6 +1,5 @@
From iris.proofmode Require Import tactics .
From iris.si_logic Require Import bi.
-Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Section si_logic_tests.
Implicit Types P Q R : siProp.
--
GitLab