Factor out the compute bit of the compute notation in curve params

This will let us call it from Ltac; notations with tactics don't internalize identifiers correctly at tactic definition time

1 files changed, 3 insertions, 1 deletions

diff --git a/src/Specific/CurveParameters.v b/src/Specific/CurveParameters.v
index 79282757d..aa679a4d3 100644
--- a/src/Specific/CurveParameters.v
+++ b/src/Specific/CurveParameters.v
@@ -45,8 +45,10 @@ Module FillCurveParameters (P : CurveParameters).
         | Some v => v
         | None => default
         end).
+  Ltac do_compute v :=
+    let v' := (eval vm_compute in v) in v'.
   Notation compute v
-    := (ltac:(let v' := v in let v' := (eval vm_compute in v') in exact v'))
+    := (ltac:(let v' := do_compute v in exact v'))
          (only parsing).
   Definition sz := P.sz.
   Definition bitwidth := P.bitwidth.