From 28508c6fa3ee811d8e51f365cd6cbdabe96352cd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 22 Oct 2017 16:09:02 -0400 Subject: Add another unfolding database --- src/Arithmetic/Core.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Arithmetic/Core.v') 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) -- cgit v1.2.3