From f14d064555ce95f642405f479066dd9f7996be06 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 3 Jan 2021 14:56:39 -0500 Subject: [PATCH] Update for Coq 8.12.2 --- DataAbstraction.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/DataAbstraction.v b/DataAbstraction.v index 6616a2a..bc371f7 100644 --- a/DataAbstraction.v +++ b/DataAbstraction.v @@ -629,7 +629,7 @@ Module AlgebraicWithEquivalenceRelation. equality. unfold equiv, elements. simplify. - SearchAbout app cons nil. + Search app cons nil. apply app_inj_tail. rewrite <- app_assoc. rewrite <- app_assoc. @@ -1547,7 +1547,7 @@ Module NatRangeSet <: FINITE_SET with Definition key := nat. unfold member, add; simplify. cases s. - SearchAbout Compare_dec.leb. + Search Compare_dec.leb. rewrite Compare_dec.leb_correct. equality. linear_arithmetic.