diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-08 21:37:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-08 21:37:24 -0400 |
| commit | 77834ca6ca1be3e707bb4951cc5cc782718c81f8 (patch) | |
| tree | 6413d0974d7ae8b76a9467ad0f3f70183b5b85e7 /src | |
| parent | 05c63d76aab155c5f57779ef1fcdb984bc5120bf (diff) | |
Fix broken implicits
Closes #190
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/Karatsuba.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v index 07171ea04..dc2f42d44 100644 --- a/src/Specific/Karatsuba.v +++ b/src/Specific/Karatsuba.v @@ -164,7 +164,7 @@ Section Ops51. do_replace_match_with_destructuring_match_in_goal. reflexivity. Defined. - + Definition goldilocks_mul_for_bounds_checker_sig : {mul : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, @@ -201,7 +201,7 @@ Section Ops51. F_mod_eq; transitivity (Positional.eval wt x); repeat autounfold; - [ + [ | autorewrite with uncps push_id push_basesystem_eval; apply goldilocks_mul_correct; try assumption; cbv; congruence ]. cbv [mod_eq]; apply f_equal2; @@ -210,7 +210,7 @@ Section Ops51. transitivity (id_with_alt_bounds_and_proof (pf := goldilocks_mul_sig_equiv a b) ((proj1_sig goldilocks_mul_sig) a b) ((proj1_sig goldilocks_mul_for_bounds_checker_sig) a b)). { cbv [proj1_sig goldilocks_mul_for_bounds_checker_sig goldilocks_mul_sig]. reflexivity. } { cbv [id_with_alt_bounds_and_proof id_with_alt_bounds]. - rewrite (proj2_sig goldilocks_mul_sig). reflexivity. } + rewrite (proj2_sig goldilocks_mul_sig). reflexivity. } Defined. Definition square_sig : @@ -279,7 +279,7 @@ Section Ops51. pose proof div_mod. pose proof wt_divides_full_pos. pose proof wt_multiples. pose proof div_correct. pose proof modulo_correct. - let x := constr:(freeze (n:=sz) (div:=div) (modulo:=modulo) wt (Z.ones bitwidth) m_enc a) in + let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in F_mod_eq; transitivity (Positional.eval wt x); repeat autounfold; [ | autorewrite with uncps push_id push_basesystem_eval; |