From 4d11f709fb93e7dd3dd1320cec945cc0dca55fec Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 31 Mar 2017 19:50:33 -0400 Subject: Fix inversion_base_type --- src/Reflection/Z/Syntax/Equality.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Reflection/Z/Syntax/Equality.v b/src/Reflection/Z/Syntax/Equality.v index 061785f29..c04f50fe2 100644 --- a/src/Reflection/Z/Syntax/Equality.v +++ b/src/Reflection/Z/Syntax/Equality.v @@ -158,7 +158,7 @@ Section encode_decode. End encode_decode. Ltac induction_type_in_using H rect := - induction H as [H] using (rect _ _ _); + induction H as [H] using (rect _ _); cbv [base_type_code] in H; let H1 := fresh H in let H2 := fresh H in -- cgit v1.2.3