From 4717443c519f5d6426c165de545952b2b7ef50f9 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr>
Date: Tue, 7 Jul 2015 18:07:31 +0200
Subject: Change the definition of Typles.tuple

---
 cparser/validator/Tuples.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'cparser')

diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v
index 88dc46e9..3fd2ec03 100644
--- a/cparser/validator/Tuples.v
+++ b/cparser/validator/Tuples.v
@@ -26,8 +26,11 @@ Definition arrows_right: Type -> list Type -> Type :=
   fold_right (fun A B => A -> B).
 
 (** A tuple is a heterogeneous list. For convenience, we use pairs. **)
-Definition tuple (types:list Type) : Type :=
-  fold_right prod unit types.
+Fixpoint tuple (types : list Type) : Type :=
+  match types with
+  | nil => unit
+  | t::q => prod t (tuple q)
+  end.
 
 Fixpoint uncurry {args:list Type} {res:Type}:
   arrows_left args res -> tuple args -> res :=
-- 
cgit