diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-09 14:50:06 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-09 14:50:06 -0500 |
| commit | 22393a2cc2cfac8dc41e94dfb3a7915b2325437a (patch) | |
| tree | c3247bfdca5e2f5e1636809fa6deefd223cacf51 /src/Util/Tuple.v | |
| parent | 970f0d7ee4d73cb4950fe7646dfe9cebc0789bf0 (diff) | |
Fix bug in 8.4
Diffstat (limited to 'src/Util/Tuple.v')
| -rw-r--r-- | src/Util/Tuple.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 |