diff --git a/theories/hlist.v b/theories/hlist.v
index 8f017fdfcd79925e5442efdda34c4b08dad9b198..1e0f9103706e8e98cd1f23e1cb93316fba753d31 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 35d7355f86ab534a907f06f7952c7282d4a6c2a6..2b892d5a6a6f4317b3a609e2f20db6fbf471b81a 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 :=