diff options
author | Jason Gross <jgross@mit.edu> | 2019-04-05 19:25:41 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-04-05 19:25:41 -0400 |
commit | de6be31e9e0f6be7ca2f61159d6a5a0e6f3969be (patch) | |
tree | 43dd790f32629266ebf0ec6332e2fe486617da6b | |
parent | 950bf3e1db4cb6920f5cd406510e17ad6a6a2cc1 (diff) |
Fix for 8.8
-rw-r--r-- | src/UnderLetsProofs.v | 4 |
1 files changed, 2 insertions, 2 deletions
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} |