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
9e80cf97
Commit
9e80cf97
authored
7 years ago
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fixes for Coq 8.6
parent
c35c95d6
Changes
4
Show whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
7 additions
and
13 deletions
+7
-13
GeneralRec.v
src/GeneralRec.v
+0
-8
Match.v
src/Match.v
+1
-1
Reflection.v
src/Reflection.v
+3
-3
Universes.v
src/Universes.v
+3
-1
No files found.
src/GeneralRec.v
View file @
9e80cf97
...
...
@@ -822,10 +822,6 @@ Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
match
goal
with
|
[
H
:
Bnd
_
_
=
Bnd
_
_
|-
_
]
=>
injection
H
;
clear
H
;
intros
;
try
subst
end
.
move
H3
after
A
.
generalize
dependent
B0
.
do
2
intro
.
subst
.
crush
.
inversion
H
;
clear
H
;
crush
.
eauto
.
...
...
@@ -839,10 +835,6 @@ Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
match
goal
with
|
[
H
:
Bnd
_
_
=
Bnd
_
_
|-
_
]
=>
injection
H
;
clear
H
;
intros
;
try
subst
end
.
move
H3
after
B
.
generalize
dependent
B0
.
do
2
intro
.
subst
.
crush
.
inversion
H0
;
clear
H0
;
crush
.
eauto
.
...
...
This diff is collapsed.
Click to expand it.
src/Match.v
View file @
9e80cf97
...
...
@@ -444,7 +444,7 @@ Ltac map T f :=
Sometimes
we
need
to
employ
the
opposite
direction
of
"nonterminal escape,"
when
we
want
to
pass
a
complicated
tactic
expression
as
an
argument
to
another
tactic
,
as
we
might
want
to
do
in
invoking
%
\
coqdocvar
{%
#
<
tt
>
#
map
#
</
tt
>
#
%}%.
*
)
Goal
False
.
let
ls
:=
map
(
nat
*
nat
)
%
type
ltac
:
(
fun
x
=>
constr
:
(
x
,
x
))
(
1
::
2
::
3
::
nil
)
in
let
ls
:=
map
(
nat
*
nat
)
%
type
ltac
:
(
fun
x
=>
constr
:
(
(
x
,
x
)
))
(
1
::
2
::
3
::
nil
)
in
pose
ls
.
(
**
[[
l
:=
(
1
,
1
)
::
(
2
,
2
)
::
(
3
,
3
)
::
nil
:
list
(
nat
*
nat
)
...
...
This diff is collapsed.
Click to expand it.
src/Reflection.v
View file @
9e80cf97
...
...
@@ -673,7 +673,7 @@ Ltac addToList x xs :=
let
b
:=
inList
x
xs
in
match
b
with
|
true
=>
xs
|
false
=>
constr
:
(
x
,
xs
)
|
false
=>
constr
:
(
(
x
,
xs
)
)
end
.
(
**
Now
we
can
write
our
recursive
function
to
calculate
the
list
of
variable
values
we
will
want
to
use
to
represent
a
term
.
*
)
...
...
@@ -718,8 +718,8 @@ Inductive formula' : Set :=
Ltac
reifyTerm
xs
e
:=
match
e
with
|
True
=>
constr
:
Truth
'
|
False
=>
constr
:
Falsehood
'
|
True
=>
Truth
'
|
False
=>
Falsehood
'
|
?
e1
/
\
?
e2
=>
let
p1
:=
reifyTerm
xs
e1
in
let
p2
:=
reifyTerm
xs
e2
in
...
...
This diff is collapsed.
Click to expand it.
src/Universes.v
View file @
9e80cf97
...
...
@@ -1068,7 +1068,9 @@ Lemma proj1_again' : forall r, proof r
The
first
goal
looks
reasonable
.
Hypothesis
[
H0
]
is
clearly
contradictory
,
as
[
discriminate
]
can
show
.
*
)
discriminate
.
try
discriminate
.
(
*
Note
:
Coq
8.6
is
now
solving
this
subgoal
automatically
!
*
This
line
left
here
to
keep
everything
working
in
*
8.4
,
8.5
,
and
8.6
.
*
)
(
**
%
\
vspace
{-
.15
in
}%
[[
H
:
proof
p
H1
:
And
p
q
=
And
p0
q0
...
...
This diff is collapsed.
Click to expand it.
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