From f65318d2036ebe26d1c537f2fd04410b32d4ff86 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Oct 2014 11:32:56 +0200
Subject: Revert "test-suite: New names for vars but the expected invariant is
 preserved"

This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf.

Going back to the convention of naming bound variables in hypotheses
of the goal as in 8.4.

My arguments for the revert are:

- apply ... with (id:=...) would have to be changed too, then possibly
  breaking the compatibility
- the naming became dependent of the order of variables as in

x:nat
H:forall x0, x0=0
=====
goal

but

H:forall x, x=0
x:nat
=====
goal

Accordingly, this is all a matter of convention, since the meaning of
bindings is anyway the same in both cases.
---
 test-suite/output/Naming.out | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index df5100631b..105940a45d 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -11,7 +11,7 @@
   x1 : nat
   x4 : nat
   x0 : nat
-  H : forall x5 x6 : nat, x5 + x1 = x4 + x6
+  H : forall x x3 : nat, x + x1 = x4 + x3
   ============================
    x + x1 = x4 + x0
 1 subgoal
@@ -51,9 +51,9 @@
   x1 : nat
   x4 : nat
   x0 : nat
-  H : forall x5 x6 : nat,
-      x5 + x1 = x4 + x6 ->
-      forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)
+  H : forall x x3 : nat,
+      x + x1 = x4 + x3 ->
+      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
   H0 : x + x1 = x4 + x0
   ============================
    forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
@@ -64,9 +64,9 @@
   x1 : nat
   x4 : nat
   x0 : nat
-  H : forall x5 x6 : nat,
-      x5 + x1 = x4 + x6 ->
-      forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)
+  H : forall x x3 : nat,
+      x + x1 = x4 + x3 ->
+      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
   H0 : x + x1 = x4 + x0
   x5 : nat
   x6 : nat
@@ -78,6 +78,6 @@
   
   x3 : nat
   a : nat
-  H : a = 0 -> forall a0 : nat, a0 = 0
+  H : a = 0 -> forall a : nat, a = 0
   ============================
    a = 0
-- 
cgit v1.2.3