From 58fb58b14106dff1b6461c0a53f8be1464e13209 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Fri, 26 Aug 2022 15:23:23 +0200
Subject: [PATCH] remove commented code
---
theories/logrel/F_mu_ref_conc/binary/logrel.v | 17 -----------------
1 file changed, 17 deletions(-)
diff --git a/theories/logrel/F_mu_ref_conc/binary/logrel.v b/theories/logrel/F_mu_ref_conc/binary/logrel.v
index 9b07826f..83746b9d 100644
--- a/theories/logrel/F_mu_ref_conc/binary/logrel.v
+++ b/theories/logrel/F_mu_ref_conc/binary/logrel.v
@@ -9,23 +9,6 @@ From iris_examples.logrel.F_mu_ref_conc Require Export typing.
From iris.prelude Require Import options.
Import uPred.
-(* (* HACK: move somewhere else *) *)
-(* Ltac auto_equiv := *)
-(* (* Deal with "pointwise_relation" *) *)
-(* repeat lazymatch goal with *)
-(* | |- pointwise_relation _ _ _ _ => intros ? *)
-(* end; *)
-(* (* Normalize away equalities. *) *)
-(* repeat match goal with *)
-(* | H : _ ≡{_}≡ _ |- _ => apply (discrete_iff _ _) in H *)
-(* | H : _ ≡ _ |- _ => apply leibniz_equiv in H *)
-(* | _ => progress simplify_eq *)
-(* end; *)
-(* (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) *)
-(* try (f_equiv; fast_done || auto_equiv). *)
-
-(* Ltac solve_proper ::= (repeat intros ?; simpl; auto_equiv). *)
-
Definition logN : namespace := nroot .@ "logN".
(** interp : is a unary logical relation. *)
--
GitLab