diff options
Diffstat (limited to 'src/Arithmetic/Core.v')
| -rw-r--r-- | src/Arithmetic/Core.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 8e7f3cb23..f3c435a09 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -995,6 +995,29 @@ End DivMod. Import B. +Create HintDb basesystem_partial_evaluation_unfolder. + +Hint Unfold + id + Positional.to_associational_cps Positional.to_associational + Positional.eval Positional.zeros Positional.add_to_nth_cps + Positional.add_to_nth Positional.place_cps Positional.place + Positional.from_associational_cps Positional.from_associational + Positional.carry_cps Positional.carry + Positional.chained_carries_cps Positional.chained_carries + Positional.sub_cps Positional.sub Positional.split_cps + Positional.scmul_cps Positional.unbalanced_sub_cps + Positional.negate_snd_cps Positional.add_cps Positional.opp_cps + Associational.eval Associational.multerm Associational.mul_cps + Associational.mul Associational.split_cps Associational.split + Associational.reduce_cps Associational.reduce + Associational.carryterm_cps Associational.carryterm + Associational.carry_cps Associational.carry + Associational.negate_snd_cps Associational.negate_snd div modulo + id_tuple_with_alt id_tuple'_with_alt + Z.add_get_carry_full + : basesystem_partial_evaluation_unfolder. + Ltac basesystem_partial_evaluation_unfolder t := eval cbv |