diff options
| author | Brian Campbell | 2020-02-05 21:53:48 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-02-05 21:53:55 +0000 |
| commit | da1309632d35c910a6d3ae14ad2f5af037fce89e (patch) | |
| tree | b54d2bfd49d18537287db82f4597d6af9631b335 | |
| parent | d4fc0ac3ced52d28a1046b6fdfc45d7c8c0afd56 (diff) | |
Tweak Coq scopes for 8.11
| -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 ( |