diff options
| -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} |