From bf999b6bb70f710c0b525fada051d1f511557daf Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Mon, 14 Jun 2021 15:32:18 +0200
Subject: [PATCH] fix compliation
---
theories/experimental/helping/helping_stack.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/experimental/helping/helping_stack.v b/theories/experimental/helping/helping_stack.v
index ad8ae29..d160868 100644
--- a/theories/experimental/helping/helping_stack.v
+++ b/theories/experimental/helping/helping_stack.v
@@ -188,7 +188,7 @@ Section offerReg_rules.
symmetry. apply agree_included.
by apply to_agree_included.
+ rewrite lookup_singleton_ne; eauto.
- by rewrite left_id. }
+ simpl. by case_match. }
by rewrite Hfoo.
Qed.
--
GitLab