From 8369340421eaf31bf82ca545209352904c2853d1 Mon Sep 17 00:00:00 2001 From: Simon Gregersen <gregersen@cs.au.dk> Date: Fri, 10 Jul 2020 15:58:07 +0200 Subject: [PATCH] fix imports --- theories/aneris_lang/lib/assert.v | 2 +- theories/aneris_lang/lib/bag.v | 2 +- theories/aneris_lang/lib/dictionary.v | 2 +- theories/aneris_lang/lib/lock.v | 2 +- theories/aneris_lang/lib/network_helpers.v | 2 +- theories/aneris_lang/lib/nodepar.v | 2 +- theories/aneris_lang/lib/serialization/serialization_base.v | 2 +- theories/aneris_lang/lib/vector_clock/vector_clock.v | 2 +- theories/aneris_lang/system_state.v | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) diff --git a/theories/aneris_lang/lib/assert.v b/theories/aneris_lang/lib/assert.v index a5c6ad5..bb51367 100644 --- a/theories/aneris_lang/lib/assert.v +++ b/theories/aneris_lang/lib/assert.v @@ -1,6 +1,6 @@ From iris.program_logic Require Export weakestpre. From iris.proofmode Require Import tactics. -From aneris Require Import lang lifting tactics proofmode notation. +From aneris.aneris_lang Require Import lang lifting tactics proofmode notation. Section code. diff --git a/theories/aneris_lang/lib/bag.v b/theories/aneris_lang/lib/bag.v index 39ae9dd..dc2116e 100644 --- a/theories/aneris_lang/lib/bag.v +++ b/theories/aneris_lang/lib/bag.v @@ -3,7 +3,7 @@ From iris.algebra Require Import excl. From iris.base_logic.lib Require Export invariants. From iris.program_logic Require Export weakestpre. From iris.proofmode Require Import coq_tactics reduction. -From aneris Require Import lang lifting tactics proofmode notation. +From aneris.aneris_lang Require Import lang lifting tactics proofmode notation. From aneris.aneris_lang.lib Require Import lock. Definition newbag : ground_lang.val := diff --git a/theories/aneris_lang/lib/dictionary.v b/theories/aneris_lang/lib/dictionary.v index bcccbaa..618a6cf 100644 --- a/theories/aneris_lang/lib/dictionary.v +++ b/theories/aneris_lang/lib/dictionary.v @@ -1,6 +1,6 @@ From stdpp Require Export strings list pretty gmap. From iris.proofmode Require Import tactics. -From aneris Require Import lang network notation tactics proofmode lifting. +From aneris.aneris_lang Require Import lang network notation tactics proofmode lifting. From aneris.aneris_lang.lib Require Import list. Module dict. diff --git a/theories/aneris_lang/lib/lock.v b/theories/aneris_lang/lib/lock.v index 2572017..9c0bca0 100644 --- a/theories/aneris_lang/lib/lock.v +++ b/theories/aneris_lang/lib/lock.v @@ -3,7 +3,7 @@ From iris.algebra Require Import excl. From iris.base_logic.lib Require Export invariants. From iris.program_logic Require Export weakestpre. From iris.proofmode Require Import coq_tactics reduction. -From aneris Require Import lang lifting tactics proofmode notation. +From aneris.aneris_lang Require Import lang lifting tactics proofmode notation. Definition newlock : ground_lang.val := λ: <>, ref #false. Definition try_acquire : ground_lang.val := λ: "l", CAS "l" #false #true. diff --git a/theories/aneris_lang/lib/network_helpers.v b/theories/aneris_lang/lib/network_helpers.v index 20e2e3f..855d519 100644 --- a/theories/aneris_lang/lib/network_helpers.v +++ b/theories/aneris_lang/lib/network_helpers.v @@ -1,6 +1,6 @@ From iris.program_logic Require Export weakestpre. From iris.proofmode Require Import tactics. -From aneris Require Import lang lifting tactics proofmode notation. +From aneris.aneris_lang Require Import lang lifting tactics proofmode notation. From aneris.aneris_lang.lib Require Import assert. Section code. diff --git a/theories/aneris_lang/lib/nodepar.v b/theories/aneris_lang/lib/nodepar.v index ecbf4e7..638f6c9 100644 --- a/theories/aneris_lang/lib/nodepar.v +++ b/theories/aneris_lang/lib/nodepar.v @@ -1,7 +1,7 @@ From iris.base_logic.lib Require Export invariants. From iris.proofmode Require Import tactics. From iris.algebra Require Import excl. -From aneris Require Export lang lifting network notation tactics proofmode. +From aneris.aneris_lang Require Export lang lifting network notation tactics proofmode. Set Default Proof Using "Type". Notation "( n1 ; ip1 ; e1 ) ||| ( n2 ; ip2 ; e2 )" := diff --git a/theories/aneris_lang/lib/serialization/serialization_base.v b/theories/aneris_lang/lib/serialization/serialization_base.v index ee9eb53..48065e0 100644 --- a/theories/aneris_lang/lib/serialization/serialization_base.v +++ b/theories/aneris_lang/lib/serialization/serialization_base.v @@ -1,7 +1,7 @@ From stdpp Require Import base pretty. From iris.program_logic Require Export weakestpre. From iris.proofmode Require Import coq_tactics tactics. -From aneris Require Import lang lifting tactics proofmode notation network. +From aneris.aneris_lang Require Import lang lifting tactics proofmode notation network. Set Default Proof Using "Type". diff --git a/theories/aneris_lang/lib/vector_clock/vector_clock.v b/theories/aneris_lang/lib/vector_clock/vector_clock.v index d73d84d..31f5c33 100644 --- a/theories/aneris_lang/lib/vector_clock/vector_clock.v +++ b/theories/aneris_lang/lib/vector_clock/vector_clock.v @@ -1,5 +1,5 @@ From stdpp Require Export base list. -From aneris Require Import lang lifting tactics proofmode notation adequacy. +From aneris.aneris_lang Require Import lang lifting tactics proofmode notation adequacy. From aneris.aneris_lang.lib Require Export util network_helpers list. From aneris.aneris_lang.lib.serialization Require Export serialization. From aneris.aneris_lang.lib.vector_clock Require Export time. diff --git a/theories/aneris_lang/system_state.v b/theories/aneris_lang/system_state.v index 116045e..989aa93 100644 --- a/theories/aneris_lang/system_state.v +++ b/theories/aneris_lang/system_state.v @@ -3,7 +3,7 @@ From iris.base_logic Require Export gen_heap. From iris.base_logic.lib Require Export own. From iris.base_logic.lib Require Import fractional. From iris.proofmode Require Import tactics. -From aneris Require Export lang network. +From aneris.aneris_lang Require Export lang network. Set Default Proof Using "Type". Import uPred. Import Network. -- GitLab