diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-07-08 19:03:05 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-07-08 20:46:01 -0400 |
| commit | 699c7964f388e0ec232f4b71096294250cd6e4cd (patch) | |
| tree | 375a12e2fdf4c57398af669b6b8ae0d8c6e82a0e /src/Arithmetic | |
| parent | b706a5f54b1dd406cae3bfbf719f22889dd23264 (diff) | |
Add cbv_runtime in Arithmetic/Core
This way, files importing Core don't have to keep track of the list of runtime operations, for unfoling.
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/Core.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 457a85a98..854b912df 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -310,6 +310,8 @@ Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope. Definition runtime_lor := Z.lor. Global Arguments runtime_lor (_ _)%RT. +Ltac cbv_runtime := cbv beta delta [runtime_add runtime_and runtime_lor runtime_mul runtime_opp runtime_shr]. + Module B. Definition limb := (Z*Z)%type. (* position coefficient and run-time value *) Module Associational. |