diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v index cfd8a294ab1493c6faf43b69dbdddde4f7181495..ffe5550f413b90fe13fb754da1724e6da8c8f59f 100644 --- a/theories/logic/spec_ra.v +++ b/theories/logic/spec_ra.v @@ -7,8 +7,8 @@ From iris.proofmode Require Import tactics. From iris.heap_lang Require Import lang lifting. Import uPred. -Definition logrelN := nroot .@ "logrel". -Definition specN := logrelN .@ "spec". +Definition relocN := nroot .@ "reloc". +Definition specN := relocN .@ "spec". (** The CMRA for the heap of the specification. *) Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC).