Turn some non-recursive `Fixpoint`s into `Definition`s.

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 :=

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 :=