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
fd192eff
Commit
fd192eff
authored
Jun 16, 2019
by
Robbert Krebbers
Browse files
Merge branch 'fixiEvalprecedence' into 'master'
Fix parsing precedence for iEval See merge request
!269
parents
0ecb5b49
cec53bd4
Pipeline
#17604
passed with stage
in 13 minutes and 54 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
tests/proofmode.ref
View file @
fd192eff
...
...
@@ 126,7 +126,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P ∗ False)%I wi
: string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
"iEval (tactic
3
) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
"test_iFrame_later_1"
...
...
@@ 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.v
View file @
fd192eff
...
...
@@ 480,6 +480,13 @@ Proof.
done
.
Qed
.
Lemma
test_iEval_precedence
:
True
⊢
True
:
PROP
.
Proof
.
iIntros
.
(* Ensure that in [iEval (a); b], b is not parsed as part of the argument of [iEval]. *)
iEval
(
rewrite
/=)
;
iPureIntro
;
exact
I
.
Qed
.
Check
"test_iSimpl_in"
.
Lemma
test_iSimpl_in
x
y
:
⌜
(
3
+
x
)%
nat
=
y
⌝

∗
⌜
S
(
S
(
S
x
))
=
y
⌝
:
PROP
.
Proof
.
iIntros
"H"
.
iSimpl
in
"H"
.
Show
.
done
.
Qed
.
...
...
tests/proofmode_iris.ref
View file @
fd192eff
...
...
@@ 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 @
fd192eff
...
...
@@ 195,7 +195,7 @@ Tactic Notation "iClear" "(" ident_list(xs) ")" constr(Hs) :=
iClear
Hs
;
clear
xs
.
(** ** Simplification *)
Tactic
Notation
"iEval"
tactic
(
t
)
:
=
Tactic
Notation
"iEval"
tactic
3
(
t
)
:
=
iStartProof
;
eapply
tac_eval
;
[
let
x
:
=
fresh
in
intros
x
;
t
;
unfold
x
;
reflexivity
...
...
@@ 212,7 +212,7 @@ Local Ltac iEval_go t Hs :=

pm_reduce
;
iEval_go
t
Hs
]
end
.
Tactic
Notation
"iEval"
tactic
(
t
)
"in"
constr
(
Hs
)
:
=
Tactic
Notation
"iEval"
tactic
3
(
t
)
"in"
constr
(
Hs
)
:
=
iStartProof
;
let
Hs
:
=
iElaborateSelPat
Hs
in
iEval_go
t
Hs
.
Tactic
Notation
"iSimpl"
:
=
iEval
(
simpl
).
...
...
@@ 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
...
...
@@ 1032,7 +1032,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)

true
=>
iPoseProofCoreLem
t
as
Htmp
before_tc
(
spec_tac
()
;
[..
tac
Htmp
])

false
=>
iPoseProofCoreLem
t
as
Htmp
before_tc
(
spec_tac
()
)
;
[..
tac
Htmp
]
iPoseProofCoreLem
t
as
Htmp
before_tc
(
spec_tac
()
;
[..
tac
Htmp
]
)
end
end
.
...
...
@@ 1634,7 +1634,7 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
(* Used for generalization in iInduction and iLöb *)
Tactic
Notation
"iRevertIntros"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iRevertIntros"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
let
rec
go
Hs
:
=
lazymatch
Hs
with

[]
=>
tac
...
...
@@ 1643,56 +1643,56 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
end
in
try
iStartProof
;
let
Hs
:
=
iElaborateSelPat
Hs
in
go
Hs
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
")"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
)
;
tac
;
iIntros
(
x1
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
)
;
tac
;
iIntros
(
x1
x2
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
)
;
tac
;
iIntros
(
x1
x2
x3
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
)
;
tac
;
iIntros
(
x1
x2
x3
x4
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
")"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
ident
(
x6
)
")"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)).
Tactic
Notation
"iRevertIntros"
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iRevertIntros"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
")"
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
")"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
")"
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
")"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
"with"
tactic
(
tac
)
:
=
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
"with"
tactic
(
tac
)
:
=
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
")"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
ident
(
x6
)
")"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
""
with
tac
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
"with"
tactic
(
tac
)
:
=
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
""
with
tac
.
(** * Destruct tactic *)
...
...
@@ 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
_
_
]

_
=>
...
...
@@ 1901,7 +1901,7 @@ Ltac iHypsContaining x :=
let
Γ
s
:
=
lazymatch
goal
with

envs_entails
(
Envs
_
?
Γ
s
_
)
_
=>
Γ
s
end
in
let
Hs
:
=
go
Γ
p
x
(@
nil
ident
)
in
go
Γ
s
x
Hs
.
Tactic
Notation
"iInductionRevert"
constr
(
x
)
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iInductionRevert"
constr
(
x
)
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevertIntros
"∗"
with
(
idtac
;
...
...
@@ 2083,7 +2083,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=

_
=>
idtac
end
].
Tactic
Notation
"iLöbRevert"
constr
(
Hs
)
"with"
tactic
(
tac
)
:
=
Tactic
Notation
"iLöbRevert"
constr
(
Hs
)
"with"
tactic
3
(
tac
)
:
=
iRevertIntros
Hs
with
(
iRevertIntros
"∗"
with
tac
).
...
...
@@ 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