diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Z/Syntax/Equality.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 |