Skip to content

Commit 9502ae0

Browse files
committed
formatting for `R notation
1 parent f11aa02 commit 9502ae0

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

theories/rel.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ Proof. simpl. firstorder. Qed.
4444
where "`" is declared at level 10
4545
*)
4646
Module Import CoindNotations.
47-
Notation "` R" := (elem R) (at level 2).
47+
Notation "` R" := (elem R) (at level 2, R at level 1, format "` R").
4848
End CoindNotations.
4949

5050
Section s.

0 commit comments

Comments
 (0)