Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
c98c721b
Commit
c98c721b
authored
Apr 29, 2019
by
Robbert Krebbers
Browse files
Rename misspelled `IAnom` into `IFresh` (`IAnon` is already in use).
parent
91dfd8b9
Changes
3
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/intro_patterns.v
View file @
c98c721b
...
...
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
Inductive
intro_pat
:
=
|
IIdent
:
ident
→
intro_pat
|
I
Anom
:
intro_pat
|
I
Fresh
:
intro_pat
|
IDrop
:
intro_pat
|
IFrame
:
intro_pat
|
IList
:
list
(
list
intro_pat
)
→
intro_pat
...
...
@@ -74,7 +74,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
|
[]
=>
Some
k
|
TName
"_"
::
ts
=>
parse_go
ts
(
StPat
IDrop
::
k
)
|
TName
s
::
ts
=>
parse_go
ts
(
StPat
(
IIdent
s
)
::
k
)
|
TAno
m
::
ts
=>
parse_go
ts
(
StPat
I
Anom
::
k
)
|
TAno
n
::
ts
=>
parse_go
ts
(
StPat
I
Fresh
::
k
)
|
TFrame
::
ts
=>
parse_go
ts
(
StPat
IFrame
::
k
)
|
TBracketL
::
ts
=>
parse_go
ts
(
StList
::
k
)
|
TBar
::
ts
=>
parse_go
ts
(
StBar
::
k
)
...
...
theories/proofmode/ltac_tactics.v
View file @
c98c721b
...
...
@@ -1219,7 +1219,7 @@ Tactic Notation "iModCore" constr(H) :=
(** * Basic destruct tactic *)
Local
Ltac
iDestructHypGo
Hz
pat
:
=
lazymatch
pat
with
|
I
Anom
=>
|
I
Fresh
=>
lazymatch
Hz
with
|
IAnon
_
=>
idtac
|
INamed
?Hz
=>
let
Hz'
:
=
iFresh
in
iRename
Hz
into
Hz'
...
...
theories/proofmode/tokens.v
View file @
c98c721b
...
...
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
Inductive
token
:
=
|
TName
:
string
→
token
|
TNat
:
nat
→
token
|
TAno
m
:
token
|
TAno
n
:
token
|
TFrame
:
token
|
TBar
:
token
|
TBracketL
:
token
...
...
@@ -43,7 +43,7 @@ Definition cons_state (kn : state) (k : list token) : list token :=
Fixpoint
tokenize_go
(
s
:
string
)
(
k
:
list
token
)
(
kn
:
state
)
:
list
token
:
=
match
s
with
|
""
=>
reverse
(
cons_state
kn
k
)
|
String
"?"
s
=>
tokenize_go
s
(
TAno
m
::
cons_state
kn
k
)
SNone
|
String
"?"
s
=>
tokenize_go
s
(
TAno
n
::
cons_state
kn
k
)
SNone
|
String
"$"
s
=>
tokenize_go
s
(
TFrame
::
cons_state
kn
k
)
SNone
|
String
"["
s
=>
tokenize_go
s
(
TBracketL
::
cons_state
kn
k
)
SNone
|
String
"]"
s
=>
tokenize_go
s
(
TBracketR
::
cons_state
kn
k
)
SNone
...
...
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