From 22393a2cc2cfac8dc41e94dfb3a7915b2325437a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 9 Nov 2016 14:50:06 -0500 Subject: Fix bug in 8.4 --- src/Util/Tuple.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Util/Tuple.v') diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 016354052..79747ec2d 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -33,11 +33,12 @@ Definition rtuple T n : Type := | S n' => rtuple' T n' end. -Fixpoint rsnoc' {T n} {struct n} : forall (x : rtuple' T n) (y : T), rtuple' T (S n) +Fixpoint rsnoc' T n {struct n} : forall (x : rtuple' T n) (y : T), rtuple' T (S n) := match n return forall (x : rtuple' T n) (y : T), rtuple' T (S n) with | O => fun x y => (x, y) | S n' => fun x y => (fst x, @rsnoc' T n' (snd x) y) end. +Global Arguments rsnoc' {T n} _ _. Fixpoint assoc_right' {n T} {struct n} : tuple' T n -> rtuple' T n -- cgit v1.2.3