From 60b48f8db5afde00fbd3f82b5a06c4b3ce79445c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Oct 2016 14:18:24 -0400 Subject: Factor out cmov{l,ne} and neg This way we will have a faster build of reification things --- src/Specific/GF25519.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Specific/GF25519.v') diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index fc207c7e0..5000cec83 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -129,7 +129,7 @@ Definition zero_subst : zero = zero_ := eq_refl zero_. Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits. Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_. -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemList.neg ModularBaseSystemList.cmovl ModularBaseSystemList.cmovne. +Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemListZOperations.neg ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne. Definition app_7 {T} (f : wire_digits) (P : wire_digits -> T) : T. Proof. -- cgit v1.2.3