diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-28 16:28:07 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-07-03 19:28:55 -0400 |
| commit | c6941b1ae419ba12be9122a60a09ef41ff750fe7 (patch) | |
| tree | cb9291204160dadc88fb53a5c93530e3cb44ad1b /src | |
| parent | 0c25de529f744cf4b2d848a509cd0d869176fd6d (diff) | |
No subst01 in mulmod
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 68c8555dd..ac1edbbea 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -986,7 +986,7 @@ Module Import UnsaturatedSolinas. (* N.B. We only need [rcarry_mul] if we want to extract the Pipeline; otherwise we can just use [rcarry_mul_correct] *) Definition srcarry_mul prefix - := BoundsPipelineToStrings + := BoundsPipelineToStrings_no_subst01 prefix "carry_mul" (carry_mul_gen @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) @@ -994,7 +994,7 @@ Module Import UnsaturatedSolinas. (Some tight_bounds). Definition rcarry_mul_correct - := BoundsPipeline_correct + := BoundsPipeline_no_subst01_correct (Some loose_bounds, (Some loose_bounds, tt)) (Some tight_bounds) (carry_mulmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) s c n idxs). |