From de6be31e9e0f6be7ca2f61159d6a5a0e6f3969be Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Apr 2019 19:25:41 -0400 Subject: Fix for 8.8 --- src/UnderLetsProofs.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 457c0e596..b8e925b1c 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -977,7 +977,7 @@ Module Compilers. Qed. End for_interp. - Section for_interp2. + Section for_interp2'. Context {base_interp1 base_interp2 : base_type -> Type} {ident_interp1 : forall t, ident t -> type.interp base_interp1 t} {ident_interp2 : forall t, ident t -> type.interp base_interp2 t}. @@ -994,7 +994,7 @@ Module Compilers. rewrite <- List.app_assoc; cbn [List.app]. eassumption. Qed. - End for_interp2. + End for_interp2'. Section with_var2_for_interp. Context {base_interp : base_type -> Type} -- cgit v1.2.3