diff options
Diffstat (limited to 'common/Memory.v')
| -rw-r--r-- | common/Memory.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/common/Memory.v b/common/Memory.v index 04a3dda..bfaf67d 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -36,6 +36,10 @@ Require Import Values. Require Export Memdata. Require Export Memtype. +(* To avoid useless definitions of inductors in extracted code. *) +Local Unset Elimination Schemes. +Local Unset Case Analysis Schemes. + Local Notation "a # b" := (ZMap.get b a) (at level 1). Module Mem <: MEM. |