diff options
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v index 9970dcd5..1f176ad9 100644 --- a/lib/coq/Sail2_operators_mwords.v +++ b/lib/coq/Sail2_operators_mwords.v @@ -8,6 +8,7 @@ Require Import Arith. Require Import ZArith. Require Import Omega. Require Import Eqdep_dec. +Open Scope Z. Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q. refine ( |