diff --git a/coq-cheri-capabilities.opam b/coq-cheri-capabilities.opam index ed526ff..8cbce7a 100644 --- a/coq-cheri-capabilities.opam +++ b/coq-cheri-capabilities.opam @@ -30,4 +30,4 @@ build: [ "@doc" {with-doc} ] ] -dev-repo: "git+https://github.com/rems-project/coq-cheri-capabilities.git" +dev-repo: "git+https://github.com/rems-project/coq-cheri-capabilities.git#replacing_coq-sail_with_coq-sail-stdpp" diff --git a/theories/Morello/Capabilities.v b/theories/Morello/Capabilities.v index a3049a0..8367ed7 100644 --- a/theories/Morello/Capabilities.v +++ b/theories/Morello/Capabilities.v @@ -1124,7 +1124,7 @@ Module Capability <: CAPABILITY (AddressValue) (Flags) (ObjType) (SealType) (Bou End Capability. -(* Module TestCaps. +Module ExampleCaps. (* c1 corresponds to https://www.morello-project.org/capinfo?c=1900000007f1cff1500000000ffffff15 *) Definition c1:Capability.t := Capability.of_Z 0x1900000007f1cff1500000000ffffff15. @@ -1140,4 +1140,4 @@ End Capability. Definition c3_bytes := ["208"%char;"230"%char;"255"%char;"255"%char;"000"%char;"000"%char;"000"%char; "042"%char;"208"%char;"230"%char;"212"%char;"102"%char;"000"%char;"000"%char;"000"%char;"220"%char]. -End TestCaps. *) +End ExampleCaps.