diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-31 19:50:33 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-31 19:50:33 -0400 |
| commit | 4d11f709fb93e7dd3dd1320cec945cc0dca55fec (patch) | |
| tree | f23858b782c1cb410508d2261962ee3ef513a71d /src | |
| parent | 69ea7992ca6a40502a33ae2a26e34575f2bd209f (diff) | |
Fix inversion_base_type
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 |