--- ./configure.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./configure	2012-08-27 16:04:19.054123072 -0600
@@ -2739,7 +2739,7 @@ $as_echo "$COQVERSION" >&6; }
 	WHYLIBCOQ=lib/coq
 	cp -f lib/coq-v7/WhyCoqDev.v lib/coq-v7/WhyCoqCompat.v
 	case $COQVERSION in
-	8.1*|8.2*|8.3*|trunk)
+	8.1*|8.2*|8.3*|8.4*|trunk)
 	  JESSIELIBCOQ=lib/coq/jessie_why.vo
 	  cp -f lib/coq/WhyCoqDev.v lib/coq/WhyCoqCompat.v
           # useful ??? [VP] Yes, the hack for making the output compliant with
--- ./lib/coq/WhyTuples.v.orig	2012-07-19 12:33:10.000000000 -0600
+++ ./lib/coq/WhyTuples.v	2012-08-27 16:03:58.726126152 -0600
@@ -20,11 +20,9 @@
 
 Definition tuple_1 (X:Set) := X.
 
-Definition tuple_2 := prod.
-Definition Build_tuple_2 := pair.
+Record tuple_2 (T1 T2:Set) : Set :=
+  {proj_2_1 : T1; proj_2_2 : T2}.
 Implicit Arguments Build_tuple_2.
-Definition proj_2_1 := fst.
-Definition proj_2_2 := snd.
 
 Record tuple_3 (T1 T2 T3:Set) : Set := 
   {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}.