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
Rodolphe Lepigre
stdpp
Commits
37133eec
Commit
37133eec
authored
Feb 20, 2019
by
Ralf Jung
Browse files
Merge branch 'ci/ralf/warnings' into 'master'
fix or silence Coq 8.10 warnings See merge request
iris/stdpp!52
parents
3c484ebe
a3bcb51e
Changes
2
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
37133eec
-Q theories stdpp
# "Declare Scope" does not exist yet in 8.9
-arg -w -arg -undeclared-scope
theories/base.v
theories/tactics.v
theories/option.v
...
...
theories/numbers.v
View file @
37133eec
...
...
@@ -399,7 +399,7 @@ Next Obligation. intros x y; apply Qclt_not_le. Qed.
Next
Obligation
.
done
.
Qed
.
Program
Instance
Qc_lt_dec
:
RelDecision
Qclt
:
=
λ
x
y
,
if
Qclt_le_dec
x
y
then
left
_
else
right
_
.
Solve
Obligation
s
with
done
.
Next
Obligation
.
done
.
Qed
.
Next
Obligation
.
intros
x
y
;
apply
Qcle_not_lt
.
Qed
.
Instance
:
PartialOrder
(
≤
).
...
...
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