Skip to content
Snippets Groups Projects
Commit 22e341f4 authored by Jonas Kastberg's avatar Jonas Kastberg
Browse files

Fixed _CoqProject bug

parent fd433c0e
No related branches found
No related tags found
1 merge request!39Multiparty synchronous
...@@ -60,4 +60,4 @@ multi_actris/channel/proto_model.v ...@@ -60,4 +60,4 @@ multi_actris/channel/proto_model.v
multi_actris/channel/proto.v multi_actris/channel/proto.v
multi_actris/channel/channel.v multi_actris/channel/channel.v
multi_actris/channel/proofmode.v multi_actris/channel/proofmode.v
multi_actris/channel/proto_consistency_examples.v multi_actris/examples/basics.v
...@@ -11,7 +11,7 @@ From iris.algebra Require Import gmap. ...@@ -11,7 +11,7 @@ From iris.algebra Require Import gmap.
From iris.proofmode Require Import coq_tactics reduction spec_patterns. From iris.proofmode Require Import coq_tactics reduction spec_patterns.
From iris.heap_lang Require Export proofmode notation. From iris.heap_lang Require Export proofmode notation.
From multi_actris.channel Require Import proto_model. 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". Set Default Proof Using "Type".
(** * Tactics for proving contractiveness of protocols *) (** * Tactics for proving contractiveness of protocols *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment