From c2bbf00999f5ddf1ac01ea5a58c2498b066f520a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 29 Apr 2020 14:29:58 -0400 Subject: [PATCH] Update for latest Coq version --- ConcurrentSeparationLogic_template.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/ConcurrentSeparationLogic_template.v b/ConcurrentSeparationLogic_template.v index 0952e96..dc6c9f3 100644 --- a/ConcurrentSeparationLogic_template.v +++ b/ConcurrentSeparationLogic_template.v @@ -9,8 +9,8 @@ Set Asymmetric Patterns. Notation heap := (fmap nat nat). Notation locks := (set nat). -Hint Extern 1 (_ <= _) => linear_arithmetic. -Hint Extern 1 (@eq nat _ _) => linear_arithmetic. +Hint Extern 1 (_ <= _) => linear_arithmetic : core. +Hint Extern 1 (@eq nat _ _) => linear_arithmetic : core. Ltac simp := repeat (simplify; subst; propositional; try match goal with @@ -187,7 +187,7 @@ Module Import S <: SEP. t. Qed. - Hint Resolve split_empty_bwd'. + Hint Resolve split_empty_bwd' : core. Theorem extra_lift : forall (P : Prop) p, P @@ -469,7 +469,7 @@ Proof. apply try_me_first_easy. Qed. -Hint Resolve try_ptsto_first. +Hint Resolve try_ptsto_first : core. (** ** The nonzero shared counter *) @@ -740,7 +740,7 @@ Qed. (** * Soundness proof *) -Hint Resolve himp_refl. +Hint Resolve himp_refl : core. Lemma invert_Return : forall linvs {result : Set} (r : result) P Q, hoare_triple linvs P (Return r) Q @@ -755,7 +755,7 @@ Proof. rewrite IHhoare_triple; eauto. Qed. -Hint Constructors hoare_triple. +Hint Constructors hoare_triple : core. Lemma invert_Bind : forall linvs {result' result} (c1 : cmd result') (c2 : result' -> cmd result) P Q, hoare_triple linvs P (Bind c1 c2) Q