Skip to content
Snippets Groups Projects
Commit b9390e69 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove `Local` that is incompatible with Coq 8.9.

parent 799c84b1
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/bi/interface.v
+ 1
− 1
View file @ b9390e69
...@@ -16,7 +16,7 @@ Section bi_mixin. ...@@ -16,7 +16,7 @@ Section bi_mixin.
Context (bi_wand : PROP → PROP → PROP). Context (bi_wand : PROP → PROP → PROP).
Context (bi_persistently : PROP → PROP). Context (bi_persistently : PROP → PROP).
Local Bind Scope bi_scope with PROP. Bind Scope bi_scope with PROP.
Local Infix "⊢" := bi_entails. Local Infix "⊢" := bi_entails.
Local Notation "'emp'" := bi_emp : bi_scope. Local Notation "'emp'" := bi_emp : bi_scope.
Local Notation "'True'" := (bi_pure True) : bi_scope. Local Notation "'True'" := (bi_pure True) : bi_scope.
......
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