From 22e341f421adc9d9fbb7d798617e3193f7168848 Mon Sep 17 00:00:00 2001 From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com> Date: Wed, 7 Feb 2024 13:16:26 +0100 Subject: [PATCH] Fixed _CoqProject bug --- _CoqProject | 2 +- multi_actris/channel/proofmode.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/_CoqProject b/_CoqProject index 98b145e..4489ccb 100644 --- a/_CoqProject +++ b/_CoqProject @@ -60,4 +60,4 @@ multi_actris/channel/proto_model.v multi_actris/channel/proto.v multi_actris/channel/channel.v multi_actris/channel/proofmode.v -multi_actris/channel/proto_consistency_examples.v +multi_actris/examples/basics.v diff --git a/multi_actris/channel/proofmode.v b/multi_actris/channel/proofmode.v index cc8cc20..9e729ed 100644 --- a/multi_actris/channel/proofmode.v +++ b/multi_actris/channel/proofmode.v @@ -11,7 +11,7 @@ From iris.algebra Require Import gmap. From iris.proofmode Require Import coq_tactics reduction spec_patterns. From iris.heap_lang Require Export proofmode notation. From multi_actris.channel Require Import proto_model. -From multi_actris Require Export channel. +From multi_actris.channel Require Export channel. Set Default Proof Using "Type". (** * Tactics for proving contractiveness of protocols *) -- GitLab