From 70609c932e066ffab0d2e3a2a38d66e834399532 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 19:14:32 +0200 Subject: Transform non-recursive Fixpoint into Definition As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version. --- backend/Debugvar.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Debugvar.v') diff --git a/backend/Debugvar.v b/backend/Debugvar.v index 1f361030..3204dae5 100644 --- a/backend/Debugvar.v +++ b/backend/Debugvar.v @@ -92,7 +92,7 @@ Fixpoint remove_state (v: ident) (s: avail) : avail := end end. -Fixpoint set_debug_info (v: ident) (info: list (builtin_arg loc)) (s: avail) := +Definition set_debug_info (v: ident) (info: list (builtin_arg loc)) (s: avail) := match normalize_debug info with | Some a => set_state v a s | None => remove_state v s -- cgit