Skip to content
Snippets Groups Projects
Commit 6696fb9c authored by Ralf Jung's avatar Ralf Jung
Browse files

fix build

parent 67e76d84
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
.gitignore
+ 1
− 0
View file @ 6696fb9c
...@@ -8,6 +8,7 @@ ...@@ -8,6 +8,7 @@
.\#* .\#*
*~ *~
*.bak *.bak
.coqdeps.d
.coq-native/ .coq-native/
build-dep/ build-dep/
Makefile.coq Makefile.coq
......
theories/bi/fixpoint.v
+ 1
− 1
View file @ 6696fb9c
...@@ -67,7 +67,7 @@ Section least. ...@@ -67,7 +67,7 @@ Section least.
End least. End least.
Section greatest. Section greatest.
Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}. Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
Global Instance greatest_fixpoint_ne : NonExpansive (bi_greatest_fixpoint F). Global Instance greatest_fixpoint_ne : NonExpansive (bi_greatest_fixpoint F).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment