From ffb7f0cc022d1598d7d696298d8af49b2a22c0a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 28 Oct 2017 15:52:16 +0200
Subject: [PATCH] Minor beautification.

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

diff --git a/theories/finite.v b/theories/finite.v
index ab14c0e0..a44bfe75 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -72,7 +72,7 @@ Definition encode_fin `{Finite A} (x : A) : fin (card A) :=
   Fin.of_nat_lt (encode_lt_card x).
 Program Definition decode_fin `{Finite A} (i : fin (card A)) : A :=
   match Some_dec (decode_nat i) return _ with
-  | inleft (exist _ x _) => x | inright _ => _
+  | inleft (x ↾ _) => x | inright _ => _
   end.
 Next Obligation.
   intros A ?? i ?; exfalso.
diff --git a/theories/hlist.v b/theories/hlist.v
index ae4f9341..046a419d 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -40,10 +40,10 @@ Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
 Arguments hlam _ _ _ _ _ / : assert.
 
 Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
-  (fix go As xs :=
+  (fix go {As} xs :=
     match xs in hlist As return himpl As B → B with
     | hnil => λ f, f
-    | @hcons A As x xs => λ f, go As xs (f x)
+    | hcons x xs => λ f, go xs (f x)
     end) _ xs f.
 Coercion hcurry : himpl >-> Funclass.
 
-- 
GitLab