diff options
Diffstat (limited to 'src/Arithmetic/Saturated/AddSub.v')
| -rw-r--r-- | src/Arithmetic/Saturated/AddSub.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Arithmetic/Saturated/AddSub.v b/src/Arithmetic/Saturated/AddSub.v index c1c701870..e34230904 100644 --- a/src/Arithmetic/Saturated/AddSub.v +++ b/src/Arithmetic/Saturated/AddSub.v @@ -238,3 +238,14 @@ End B. Hint Opaque B.Positional.sat_sub B.Positional.sat_add B.Positional.chain_op B.Positional.chain_op' : uncps. Hint Rewrite @B.Positional.sat_sub_id @B.Positional.sat_add_id @B.Positional.chain_op_id @B.Positional.chain_op' : uncps. Hint Rewrite @B.Positional.sat_sub_mod @B.Positional.sat_sub_div @B.Positional.sat_add_mod @B.Positional.sat_add_div using (omega || assumption) : push_basesystem_eval. + +Hint Unfold + B.Positional.chain_op'_cps + B.Positional.chain_op' + B.Positional.chain_op_cps + B.Positional.chain_op + B.Positional.sat_add_cps + B.Positional.sat_add + B.Positional.sat_sub_cps + B.Positional.sat_sub + : basesystem_partial_evaluation_unfolder. |