From c9edf9a01fc1bb9678fb0853f795fc3b70ec7cde Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 29 Apr 2021 10:30:15 +0200
Subject: [PATCH] fix implicit types

---
 theories/list_numbers.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index fbf61411..d6b0b991 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -218,8 +218,8 @@ End sum_list.
 (** ** Properties of the [Z_to_little_endian] and [Z_of_little_endian] functions *)
 Section Z_little_endian.
   Local Open Scope Z_scope.
-  Implicit Types n m : nat.
-  Implicit Types z : Z.
+  Implicit Types m : nat.
+  Implicit Types n z : Z.
 
   Lemma Z_to_of_little_endian m n bs:
     m = length bs → 0 ≤ n →
-- 
GitLab