fixes #117

affeldt-aist · May 30, 2024 · 3b5abca · 3b5abca
1 parent 2911b1f
commit 3b5abca
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/probability/fdist.v b/probability/fdist.v
@@ -69,7 +69,7 @@ Require Import ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext.
 (******************************************************************************)
 
 Reserved Notation "{ 'fdist' T }" (at level 0, format "{ 'fdist'  T }").
-Reserved Notation "R '.-fdist' T" (at level 2, format "R '.-fdist' T").
+Reserved Notation "R '.-fdist' T" (at level 2, format "R '.-fdist'  T").
 Reserved Notation "'`U' C0 " (at level 10, C0 at next level).
 Reserved Notation "P `^ n" (at level 5).
 Reserved Notation "P `X W" (at level 6).