From d82f294dcc879acad5fb7e2d2fd4a48070f3f04d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 6 Jan 2021 21:32:08 +0100 Subject: Making verify_mapping_mn_rec tail recursive (should fix arm CI) #231 --- backend/Duplicate.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'backend/Duplicate.v') diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 7dea752b..40db4e45 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -203,8 +203,7 @@ Fixpoint verify_mapping_mn_rec dupmap f f' lm := match lm with | nil => OK tt | m :: lm => do u <- verify_mapping_mn dupmap f f' m; - do u2 <- verify_mapping_mn_rec dupmap f f' lm; - OK tt + verify_mapping_mn_rec dupmap f f' lm end. Definition verify_mapping_match_nodes dupmap (f f': function): res unit := -- cgit