diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-12 13:38:38 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-12 13:38:38 +0100 |
commit | b4e70337d1c0d1130ec9c98e7fe6e52dbfee46a5 (patch) | |
tree | 2446ae118e6e1cfd750e9926925bcce1e69f9255 /src/common/Vericertlib.v | |
parent | 06b24257359305114b868b5b78971cc4c6e30db1 (diff) | |
parent | 11c5cc2ce59fe68959fe424fc04d4e947432abcb (diff) | |
download | vericert-b4e70337d1c0d1130ec9c98e7fe6e52dbfee46a5.tar.gz vericert-b4e70337d1c0d1130ec9c98e7fe6e52dbfee46a5.zip |
Merge branch 'dev/scheduling' of git.ymhg.org:vericert into dev/scheduling
Diffstat (limited to 'src/common/Vericertlib.v')
-rw-r--r-- | src/common/Vericertlib.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index b58ebd4..389a74f 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -34,7 +34,7 @@ Require Import vericert.common.Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) -Local Open Scope Z_scope. +#[local] Open Scope Z_scope. (* This tactic due to Clement Pit-Claudel with some minor additions by JDP to allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) @@ -190,8 +190,8 @@ Ltac liapp := Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption; try (solve [auto]). -Global Opaque Nat.div. -Global Opaque Z.mul. +#[global] Opaque Nat.div. +#[global] Opaque Z.mul. (* Definition const (A B : Type) (a : A) (b : B) : A := a. @@ -231,7 +231,7 @@ Definition join {A : Type} (a : option (option A)) : option A := Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). + (at level 200, X name, A at level 100, B at level 200). End Notation. End Option. |