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

Fix scope for uPred_const.

parent 979b6b5b
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
program_logic/upred.v
+ 1
− 1
View file @ ff9ebff8
...@@ -208,7 +208,7 @@ Arguments uPred_holds {_} _%I _ _. ...@@ -208,7 +208,7 @@ Arguments uPred_holds {_} _%I _ _.
Arguments uPred_entails _ _%I _%I. Arguments uPred_entails _ _%I _%I.
Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope. Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
Notation "(⊑)" := uPred_entails (only parsing) : C_scope. Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
Notation "■ φ" := (uPred_const φ) (at level 20) : uPred_scope. Notation "■ φ" := (uPred_const φ%type) (at level 20) : uPred_scope.
Notation "'False'" := (uPred_const False) : uPred_scope. Notation "'False'" := (uPred_const False) : uPred_scope.
Notation "'True'" := (uPred_const True) : uPred_scope. Notation "'True'" := (uPred_const True) : uPred_scope.
Infix "∧" := uPred_and : uPred_scope. Infix "∧" := uPred_and : uPred_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