From c95596b7aa29c689a216ac83cd6fc91639470ff0 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 20 Jul 2021 08:21:26 +0200 Subject: [PATCH] Missing entry in sed script for curry MR. --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index fc7670d6..2d590c01 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -155,6 +155,7 @@ s/\bgmap_curry_uncurry\b/gmap_uncurry_curry/g s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g s/\bhcurry_uncurry\b/huncurry_curry/g +s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g ' $(find theories -name "*.v") ``` -- GitLab