diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-07-01 11:46:34 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-07-01 11:56:02 -0400 |
| commit | e301cc689ec630bb5e6c3c3d3a234dcee2652028 (patch) | |
| tree | 4435694a75a4b2a288f33aed8de319c2c2f3dc84 /src/Arithmetic/Saturated | |
| parent | 2fafbe93470ad2971612a1cd4d0a9d507f35e548 (diff) | |
change opp to runtime_opp
Diffstat (limited to 'src/Arithmetic/Saturated')
| -rw-r--r-- | src/Arithmetic/Saturated/MontgomeryAPI.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v index 334a009e9..1c7aebca0 100644 --- a/src/Arithmetic/Saturated/MontgomeryAPI.v +++ b/src/Arithmetic/Saturated/MontgomeryAPI.v @@ -78,7 +78,7 @@ Section API. B.Positional.select_cps mask (fst carry_result) r (fun selected => join0_cps selected (fun selected' => - B.Positional.sat_add_cps (s:=bound) (left_append (- fst carry_result) (snd carry_result)) selected' _ + B.Positional.sat_add_cps (s:=bound) (left_append (- (fst carry_result))%RT (snd carry_result)) selected' _ (* We can now safely discard the carry and the highest digit. This relies on the precondition that p - q + r < bound^n. *) (fun carry_result' => drop_high_cps (snd carry_result') f)))). @@ -424,7 +424,7 @@ Section API. pose proof (@uweight_le_mono _ bound_pos n (S n) (Nat.le_succ_diag_r _)). intros. repeat match goal with - | _ => progress (intros; cbv [eval sub_then_maybe_add sub_then_maybe_add_cps] in * ) + | _ => progress (intros; cbv [eval runtime_opp sub_then_maybe_add sub_then_maybe_add_cps] in * ) | _ => progress autorewrite with uncps push_id push_basesystem_eval | _ => rewrite eval_drop_high by (apply @B.Positional.small_sat_add; omega) | _ => rewrite B.Positional.sat_sub_mod by omega |