diff options
| author | Frédéric Besson | 2019-10-22 14:30:51 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-10-22 14:30:51 +0200 |
| commit | ac8633ba19a7d8e937bbd6f9b7de2ad82b89f22f (patch) | |
| tree | b6512ba01f5b00fe490fe90b9d848c0d8a4c1f80 /plugins/micromega/ZifyBool.v | |
| parent | 487f23187413e6cf6ee117d798a9057d0008aa6a (diff) | |
| parent | 4af9a79457fc265b1696de2b1fa1018ef12c986a (diff) | |
Merge PR #10875: [Stdlib] Remove some uses of the “omega” tactic
Reviewed-by: fajb
Diffstat (limited to 'plugins/micromega/ZifyBool.v')
| -rw-r--r-- | plugins/micromega/ZifyBool.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/ZifyBool.v b/plugins/micromega/ZifyBool.v index 6259c5b47a..03a7774a31 100644 --- a/plugins/micromega/ZifyBool.v +++ b/plugins/micromega/ZifyBool.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import Bool ZArith. -Require Import ZifyClasses. +Require Import Zify ZifyClasses. Local Open Scope Z_scope. (* Instances of [ZifyClasses] for dealing with boolean operators. Various encodings of boolean are possible. One objective is to |