From dff0e8a030cac148f70d6c4d77bd23103e55daed Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Fri, 20 Sep 2019 18:55:38 +0200 Subject: [PATCH] Remove "Unset Printing Notations" --- theories/typing/lib/rc/rc.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v index f351f1dd..b0ffc6ab 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 Σ := -- GitLab