Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Dmitry Khalanskiy
Iris
Commits
42f0842f
Commit
42f0842f
authored
Jun 25, 2018
by
Ralf Jung
Browse files
bump std++; test that we don't break setoid_rewrite
parent
df4beedf
Changes
2
Hide whitespace changes
Inline
Sidebyside
Showing
2 changed files
with
17 additions
and
1 deletion
+17
1
opam
opam
+1
1
tests/algebra.v
tests/algebra.v
+16
0
No files found.
opam
View file @
42f0842f
...
...
@@ 11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "rf" "%{lib}%/coq/usercontrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.9~")  (= "dev") }
"coqstdpp" { (= "dev.2018062
0.0.b2ca5d48
")  (= "dev") }
"coqstdpp" { (= "dev.2018062
5.1.0eb9a89b
")  (= "dev") }
]
tests/algebra.v
View file @
42f0842f
...
...
@@ 8,3 +8,19 @@ Section tests.
Solve
Obligations
with
solve_proper
.
End
tests
.
(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
we cannot [1]. So at least we try to make sure the first solution found
is the right one, to not pay performance in the success case [2].
[1] https://github.com/coq/coq/issues/7916
[2] https://gitlab.mpisws.org/robbertkrebbers/coqstdpp/merge_requests/38
*)
Lemma
test_setoid_rewrite
:
exists
R
,
@
Reflexive
Prop
R
/\
R
=
iff
.
Proof
.
eexists
.
split
.

apply
_
.

reflexivity
.
Qed
.
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