From a00e547f92cd34e4478f40a33739efd72889ee2a Mon Sep 17 00:00:00 2001 From: Nicolas Nardino Date: Wed, 14 Feb 2024 12:48:32 +0100 Subject: [PATCH] whitespace --- theories/input_lang_delim/interp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/input_lang_delim/interp.v b/theories/input_lang_delim/interp.v index 6d358f4..a218431 100644 --- a/theories/input_lang_delim/interp.v +++ b/theories/input_lang_delim/interp.v @@ -507,7 +507,7 @@ Section interp. #[export] Instance interp_reset_ne : NonExpansive (interp_reset). Proof. - intros n ???. rewrite /interp_reset. simpl. repeat f_equiv. + intros n ???. rewrite /interp_reset. simpl. repeat f_equiv. by do 2 (intro; simpl; repeat f_equiv). Qed.