diff options
Diffstat (limited to 'lib/Lattice.v')
| -rw-r--r-- | lib/Lattice.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/Lattice.v b/lib/Lattice.v index 51a7976..fd05b34 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -16,6 +16,10 @@ Require Import Coqlib. Require Import Maps. Require Import FSets. +(* To avoid useless definitions of inductors in extracted code. *) +Local Unset Elimination Schemes. +Local Unset Case Analysis Schemes. + (** * Signatures of semi-lattices *) (** A semi-lattice is a type [t] equipped with an equivalence relation [eq], |