Commit bc055a22 authored by Jonas Kastberg's avatar Jonas Kastberg

Removed dangling `-` that somehow did not cause compilation errors

parent 79da67c9
Pipeline #27746 passed with stage
in 5 minutes and 40 seconds
......@@ -12,7 +12,7 @@ From iris.proofmode Require Export tactics.
From actris Require Export channel.
From iris.proofmode Require Import coq_tactics reduction spec_patterns.
-(** * Tactics for proving contractiveness of protocols *)
(** * Tactics for proving contractiveness of protocols *)
Ltac f_dist_le :=
match goal with
| H : _ {?n} _ |- _ {?n'} _ => apply (dist_le n); [apply H|lia]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment