diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-20 13:26:10 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-20 13:52:18 -0400 |
| commit | 3807e854b302cfab34c68e41dd58fe3e284d1cbe (patch) | |
| tree | 264cd33246c27dd6854c9912fe8d23d99665d617 /src/Arithmetic/Saturated.v | |
| parent | edd29cfc1a99fb5e158fdea1060b762c65f732fa (diff) | |
Add conditional_sub_id to uncps globally
Diffstat (limited to 'src/Arithmetic/Saturated.v')
| -rw-r--r-- | src/Arithmetic/Saturated.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index c2a880ea6..6d12bca0b 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -737,12 +737,12 @@ Section API. B.Positional.select_cps mask (left_hd p) q (fun qq => Columns.unbalanced_sub_cps (n3:=n) (uweight bound) p qq (* We can safely discard the carry, since our preconditions tell us - that, whether or not the subtraction happened, n limbs is + that, whether or not the subtraction happened, n limbs is sufficient to store the result. *) (fun carry_result => f (snd carry_result))). Definition conditional_sub {n} mask p q := @conditional_sub_cps n mask p q _ id. - + Hint Opaque join0 divmod drop_high scmul add conditional_sub : uncps. Section CPSProofs. @@ -1048,7 +1048,7 @@ Section API. | _ => assert (p = 0) by omega; subst p; break_match; ring end. Qed. - + Lemma small_conditional_sub n mask (p:T (S n)) (q:T n) (psmall : small p) (qsmall : small q) (Hmask : Tuple.map (Z.land mask) q = q): @@ -1124,7 +1124,7 @@ Section API. End Proofs. End API. -Hint Rewrite join0_id divmod_id drop_high_id scmul_id add_id : uncps. +Hint Rewrite join0_id divmod_id drop_high_id scmul_id add_id conditional_sub_id : uncps. (* (* Just some pretty-printing *) |