From 70609c932e066ffab0d2e3a2a38d66e834399532 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
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/NeedDomain.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/NeedDomain.v')

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 3c2d8e20..d9e9e025 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -47,7 +47,7 @@ Definition iagree (p q mask: int) : Prop :=
   forall i, 0 <= i < Int.zwordsize -> Int.testbit mask i = true ->
             Int.testbit p i = Int.testbit q i.
 
-Fixpoint vagree (v w: val) (x: nval) {struct x}: Prop :=
+Definition vagree (v w: val) (x: nval) : Prop :=
   match x with
   | Nothing => True
   | I m =>
-- 
cgit