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)

1 files changed, 5 insertions, 5 deletions

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 *)