diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-22 16:09:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-22 16:09:02 -0400 |
| commit | 28508c6fa3ee811d8e51f365cd6cbdabe96352cd (patch) | |
| tree | 5aa261e20ea677cb9ad50907d7a84588a296a013 /src/Arithmetic/Core.v | |
| parent | 91c0f39a5c7236489e268de0e5fa97b055698e4c (diff) | |
Add another unfolding database
Diffstat (limited to 'src/Arithmetic/Core.v')
| -rw-r--r-- | src/Arithmetic/Core.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 5104a21aa..4df36a0aa 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1133,7 +1133,7 @@ Ltac pattern_strip_full t := let t := (eval pattern (@Let_In Z (fun _ => Z)), @Z.add_get_carry_cps, @Z.mul_split_at_bitwidth_cps, - Z.eq_dec_cps, Z.eqb_cps, + (@Z.eq_dec_cps), (@Z.eqb_cps), @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor, (@id_with_alt Z), @Z.add_get_carry, @Z.zselect, @Z.mul_split_at_bitwidth, @@ -1165,7 +1165,7 @@ Ltac apply_patterned_full t1 := (@Let_In) (@id_with_alt) (@Let_In Z (fun _ => Z)) (@Z.add_get_carry_cps) (@Z.mul_split_at_bitwidth_cps) - Z.eq_dec_cps Z.eqb_cps + (@Z.eq_dec_cps) (@Z.eqb_cps) (@runtime_mul) (@runtime_add) (@runtime_opp) (@runtime_shr) (@runtime_and) (@runtime_lor) (@id_with_alt Z) (@Z.add_get_carry) (@Z.zselect) (@Z.mul_split_at_bitwidth) |