From 2ec23bde8d4f832f834e3df51ddedeb26037430a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Jun 2020 23:31:16 +0200
Subject: [PATCH] Turn some non-recursive `Fixpoint`s into `Definition`s.

---
 theories/hlist.v  | 4 ++--
 theories/natmap.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/hlist.v b/theories/hlist.v
index 8f017fdf..1e0f9103 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -14,9 +14,9 @@ Fixpoint tapp (As Bs : tlist) : tlist :=
 Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
   match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
 
-Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
+Definition hhead {A As} (xs : hlist (tcons A As)) : A :=
   match xs with hnil => () | hcons x _ => x end.
-Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
+Definition htail {A As} (xs : hlist (tcons A As)) : hlist As :=
   match xs with hnil => () | hcons _ xs => xs end.
 
 Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
diff --git a/theories/natmap.v b/theories/natmap.v
index 35d7355f..2b892d5a 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -258,7 +258,7 @@ Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
 (* Fixpoint avoids this definition from being unfolded *)
-Fixpoint bools_to_natset (βs : list bool) : natset :=
+Definition bools_to_natset (βs : list bool) : natset :=
   let f (β : bool) := if β then Some () else None in
   Mapset $ list_to_natmap $ f <$> βs.
 Definition natset_to_bools (sz : nat) (X : natset) : list bool :=
-- 
GitLab