Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
C
cpdt
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
research
cpdt
Commits
9525a82e
Commit
9525a82e
authored
Oct 01, 2008
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Remove [done] markers after enhancement phase finishes
parent
6e8d3f27
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
12 additions
and
7 deletions
+12
-7
Coinductive.v
src/Coinductive.v
+6
-6
Tactics.v
src/Tactics.v
+6
-1
No files found.
src/Coinductive.v
View file @
9525a82e
...
@@ -413,12 +413,12 @@ Section constFold_ok.
...
@@ -413,12 +413,12 @@ Section constFold_ok.
Hint
Resolve
regmapCompat_set_None
regmapCompat_set_Some
.
Hint
Resolve
regmapCompat_set_None
regmapCompat_set_Some
.
Hint
Constructors
run
.
Hint
Constructors
run
.
cofix
.
cofix
;
destruct
1
;
crush
;
eauto
;
destruct
1
;
crush
;
eauto
;
repeat
match
goal
with
repeat
match
goal
with
|
[
H
:
regmapCompat
_
_
|-
run
_
_
(
match
get
?
RM
?
R
with
Some
_
=>
_
|
None
=>
_
end
)
_
]
=>
|
[
H
:
regmapCompat
_
_
|-
run
_
_
(
match
get
?
RM
?
R
with
Some
_
=>
_
|
None
=>
_
end
)
_
]
=>
generalize
(
H
R
)
;
destruct
(
get
RM
R
)
;
crush
generalize
(
H
R
)
;
destruct
(
get
RM
R
)
;
crush
end
.
end
.
Qed
.
Qed
.
End
constFold_ok
.
End
constFold_ok
.
...
...
src/Tactics.v
View file @
9525a82e
...
@@ -102,11 +102,16 @@ Ltac inster e trace :=
...
@@ -102,11 +102,16 @@ Ltac inster e trace :=
end
end
end
.
end
.
Ltac
un_done
:=
repeat
match
goal
with
|
[
H
:
done
_
|-
_
]
=>
clear
H
end
.
Ltac
crush
'
lemmas
invOne
:=
Ltac
crush
'
lemmas
invOne
:=
let
sintuition
:=
simpl
in
*;
intuition
;
subst
;
repeat
(
simplHyp
invOne
;
intuition
;
subst
)
;
try
congruence
let
sintuition
:=
simpl
in
*;
intuition
;
subst
;
repeat
(
simplHyp
invOne
;
intuition
;
subst
)
;
try
congruence
in
(
sintuition
;
rewriter
;
in
(
sintuition
;
rewriter
;
repeat
((
app
ltac
:
(
fun
L
=>
inster
L
L
)
lemmas
||
appHyps
ltac
:
(
fun
L
=>
inster
L
L
))
;
repeat
((
app
ltac
:
(
fun
L
=>
inster
L
L
)
lemmas
||
appHyps
ltac
:
(
fun
L
=>
inster
L
L
))
;
repeat
(
simplHyp
invOne
;
intuition
))
;
repeat
(
simplHyp
invOne
;
intuition
))
;
sintuition
;
try
omega
)
.
un_done
;
sintuition
;
try
omega
)
.
Ltac
crush
:=
crush
'
tt
fail
.
Ltac
crush
:=
crush
'
tt
fail
.
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