Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
cec53bd4
Verified
Commit
cec53bd4
authored
Jun 14, 2019
by
Paolo G. Giarrusso
Browse files
tactic>tactic3 for remaining tactics
parent
c9418149
Changes
3
Hide whitespace changes
Inline
Sidebyside
tests/proofmode.ref
View file @
cec53bd4
...
...
@@ 443,8 +443,8 @@ Tactic failure: iModIntro: spatial context is nonempty.
: string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
"iDestructCore (open_constr) as (constr) (tactic
3
)" and
"iDestructCore (open_constr) as (constr) (tactic
3
)", last call failed.
Tactic failure: iDestruct: "HQ" not found.
"iIntros_dup_name"
: string
...
...
@@ 553,14 +553,14 @@ Tactic failure: iStartProof: not a BI assertion.
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic
3
)" and
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
Tactic failure: iPoseProof: 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) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic
3
)",
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to fun H => iDestructHyp H as pat),
...
...
@@ 573,15 +573,15 @@ Tactic failure: iRename: "H" not fresh.
: string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)" 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) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic
3
)",
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"tac" (bound to spec_tac ltac:(()); [ ..  tac Htmp ]),
"spec_tac" (bound to
...
...
@@ 616,9 +616,9 @@ Tactic failure: iElaborateSelPat: "H" not found.
: string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
...
...
@@ 627,9 +627,9 @@ 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) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"iDestructCore (open_constr) as (constr) (tactic
3
)",
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
...
...
@@ 648,7 +648,7 @@ Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: cannot apply P.
...
...
@@ 656,7 +656,7 @@ Tactic failure: iApply: cannot apply P.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
...
...
@@ 665,7 +665,7 @@ not absorbing and the remaining hypotheses not affine.
: string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic
3
)",
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
...
...
tests/proofmode_iris.ref
View file @
cec53bd4
...
...
@@ 111,20 +111,20 @@
: string
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
"iInvCore (constr) in (tactic)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
"iInvCore (constr) in (tactic
3
)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic
3
)", 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 (tactic)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
"iInvCore (constr) in (tactic
3
)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic
3
)", 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 (tactic)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic)", last call
"iInvCore (constr) in (tactic
3
)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic
3
)", last call
failed.
Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
...
...
theories/proofmode/ltac_tactics.v
View file @
cec53bd4
...
...
@@ 726,7 +726,7 @@ Tactic Notation "iPoseProofCoreHyp" constr(H) "as" constr(Hnew) :=
end
.
Tactic
Notation
"iPoseProofCoreLem"
constr
(
lem
)
"as"
constr
(
Hnew
)
"before_tc"
tactic
(
tac
)
:
=
constr
(
lem
)
"as"
constr
(
Hnew
)
"before_tc"
tactic
3
(
tac
)
:
=
eapply
tac_pose_proof
with
Hnew
_;
(* (j:=H) *)
[
iIntoEmpValid
lem

pm_reduce
;
...
...
@@ 1015,7 +1015,7 @@ Both variants of [lazy_tc] are used in other tactics that build on top of
because it may be not possible to eliminate logical connectives before all
type class constraints have been resolved. *)
Tactic
Notation
"iPoseProofCore"
open_constr
(
lem
)
"as"
constr
(
p
)
constr
(
lazy_tc
)
tactic
(
tac
)
:
=
"as"
constr
(
p
)
constr
(
lazy_tc
)
tactic
3
(
tac
)
:
=
iStartProof
;
let
Htmp
:
=
iFresh
in
let
t
:
=
lazymatch
lem
with
ITrm
?t
?xs
?pat
=>
t

_
=>
lem
end
in
...
...
@@ 1710,7 +1710,7 @@ Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
Instance
copy_destruct_persistently
{
PROP
:
bi
}
(
P
:
PROP
)
:
CopyDestruct
P
→
CopyDestruct
(<
pers
>
P
)
:
=
{}.
Tactic
Notation
"iDestructCore"
open_constr
(
lem
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
Tactic
Notation
"iDestructCore"
open_constr
(
lem
)
"as"
constr
(
p
)
tactic
3
(
tac
)
:
=
let
ident
:
=
lazymatch
type
of
lem
with

ident
=>
constr
:
(
Some
lem
)
...
...
@@ 1869,7 +1869,7 @@ result in the following actions:
 Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
 Introduce the proofmode hypotheses [Hs]
*)
Tactic
Notation
"iInductionCore"
tactic
(
tac
)
"as"
constr
(
IH
)
:
=
Tactic
Notation
"iInductionCore"
tactic
3
(
tac
)
"as"
constr
(
IH
)
:
=
let
rec
fix_ihs
rev_tac
:
=
lazymatch
goal
with

H
:
context
[
envs_entails
_
_
]

_
=>
...
...
@@ 2144,7 +2144,7 @@ Tactic Notation "iLöb" "as" constr (IH) "forall" "(" ident(x1) ident(x2)
Boolean or an introduction pattern, which will be coerced into [true] if it
only contains `#` or `%` patterns at the toplevel, and [false] otherwise. *)
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
"with"
constr
(
Hs
)
"as"
constr
(
p
)
tactic
3
(
tac
)
:
=
iStartProof
;
let
pats
:
=
spec_pat
.
parse
Hs
in
lazymatch
pats
with
...
...
@@ 2156,7 +2156,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
[
pm_reduce
;
iSpecializeCore
H
with
hnil
pats
as
p
;
[..
tac
H
]].
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"as"
constr
(
p
)
tactic
3
(
tac
)
:
=
let
p
:
=
intro_pat_intuitionistic
p
in
lazymatch
p
with

true
=>
iAssertCore
Q
with
"[#]"
as
p
tac
...
...
@@ 2314,7 +2314,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
(* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
invariant. *)
Tactic
Notation
"iInvCore"
constr
(
select
)
"with"
constr
(
pats
)
"as"
open_constr
(
Hclose
)
"in"
tactic
(
tac
)
:
=
Tactic
Notation
"iInvCore"
constr
(
select
)
"with"
constr
(
pats
)
"as"
open_constr
(
Hclose
)
"in"
tactic
3
(
tac
)
:
=
iStartProof
;
let
pats
:
=
spec_pat
.
parse
pats
in
lazymatch
pats
with
...
...
@@ 2361,13 +2361,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
)].
(* Without closing view shift *)
Tactic
Notation
"iInvCore"
constr
(
N
)
"with"
constr
(
pats
)
"in"
tactic
(
tac
)
:
=
Tactic
Notation
"iInvCore"
constr
(
N
)
"with"
constr
(
pats
)
"in"
tactic
3
(
tac
)
:
=
iInvCore
N
with
pats
as
(@
None
string
)
in
ltac
:
(
tac
).
(* Without pattern *)
Tactic
Notation
"iInvCore"
constr
(
N
)
"as"
constr
(
Hclose
)
"in"
tactic
(
tac
)
:
=
Tactic
Notation
"iInvCore"
constr
(
N
)
"as"
constr
(
Hclose
)
"in"
tactic
3
(
tac
)
:
=
iInvCore
N
with
"[$]"
as
Hclose
in
ltac
:
(
tac
).
(* Without both *)
Tactic
Notation
"iInvCore"
constr
(
N
)
"in"
tactic
(
tac
)
:
=
Tactic
Notation
"iInvCore"
constr
(
N
)
"in"
tactic
3
(
tac
)
:
=
iInvCore
N
with
"[$]"
as
(@
None
string
)
in
ltac
:
(
tac
).
(* With everything *)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment