From 05c101daeef6358bfc64e5997c8b8aea7d03f30d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 28 Apr 2017 13:11:33 -0400 Subject: Fix nth_default for the tip of v8.6 This is bug #5497, https://coq.inria.fr/bugs/show_bug.cgi?id=5497, Coq v8.6 has weaker pattern matching than Coq 8.6 (regression) --- src/Util/Tuple.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 763765898..cf3ce377e 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -780,11 +780,11 @@ Lemma map_append {A B n} (f:A->B) : forall (x:tuple A n) (a:A), map f (append a x) = append (f a) (map f x). Proof. destruct n; auto using map_append'. Qed. -Fixpoint nth_default {A m} (d:A) n (x: tuple A m) : A := - match m,n with - | O, _ => d - | S m', O => hd x - | S m', S n' => nth_default d n' (tl x) +Fixpoint nth_default {A m} (d:A) n : tuple A m -> A := + match m, n with + | O, _ => fun _ => d + | S m', O => hd + | S m', S n' => fun x => nth_default d n' (tl x) end. (* map operation that carries state *) -- cgit v1.2.3