aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Core.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Arithmetic/Core.v')
-rw-r--r--src/Arithmetic/Core.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index b86ac09b9..d61ff5ba4 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -837,7 +837,7 @@ Module B.
Section Select.
Context {weight : nat -> Z}.
-
+
Definition select_cps {n} (mask cond:Z) (p:tuple Z n)
{T} (f:tuple Z n->T) :=
dlet t := Z.zselect cond 0 mask in Tuple.map_cps (runtime_and t) p f.