Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Iris
Commits
15be3526
Commit
15be3526
authored
Feb 22, 2017
by
Ralf Jung
Browse files
update std++
parent
97d4205d
Pipeline
#3955
passed with stage
in 3 minutes and 43 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
opam.pins
View file @
15be3526
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp
3103b7bf52d0275f2938d9af44ab2d0db89a6251
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp
0671cb48dd1f893c48672de216847d46d5263e04
theories/algebra/ofe.v
View file @
15be3526
...
...
@@ -222,9 +222,7 @@ Ltac f_contractive :=
end
;
try
reflexivity
.
Ltac
solve_contractive
:
=
preprocess_solve_proper
;
solve
[
repeat
(
first
[
f_contractive
|
f_equiv
]
;
try
eassumption
)].
Ltac
solve_contractive
:
=
solve_proper_core
ltac
:
(
fun
_
=>
first
[
f_contractive
|
f_equiv
]).
(** Fixpoint *)
Program
Definition
fixpoint_chain
{
A
:
ofeT
}
`
{
Inhabited
A
}
(
f
:
A
→
A
)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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