diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index f351f1dd0490a3c2f6883d0ba584658d78596fdb..b0ffc6abbbfe7321ff6f6b3342771532e23957d4 100644 --- a/theories/typing/lib/rc/rc.v +++ b/theories/typing/lib/rc/rc.v @@ -6,8 +6,6 @@ From lrust.typing Require Export type. From lrust.typing Require Import typing option. Set Default Proof Using "Type". -Unset Printing Notations. - Definition rc_stR := prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR. Class rcG Σ :=