From bd34d676010ebf6dd4aa5076537f89572803dd3d Mon Sep 17 00:00:00 2001 From: jadep Date: Wed, 3 Apr 2019 14:45:32 -0400 Subject: partition -> Partition.partition to prevent confusion with List.partition --- src/PushButtonSynthesis/WordByWordMontgomery.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/PushButtonSynthesis/WordByWordMontgomery.v') diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index ebf250664..ea67f8b9c 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -103,9 +103,9 @@ Section __. end. Let n_bytes := bytes_n machine_wordsize 1 n. Let prime_upperbound_list : list Z - := partition (uweight machine_wordsize) n (s-1). + := Partition.partition (uweight machine_wordsize) n (s-1). Let prime_bytes_upperbound_list : list Z - := partition (weight 8 1) n_bytes (s-1). + := Partition.partition (weight 8 1) n_bytes (s-1). Let upperbounds : list Z := prime_upperbound_list. Definition prime_bound : ZRange.type.option.interp (base.type.Z) := Some r[0~>m-1]%zrange. -- cgit v1.2.3