From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/output/Naming.v | 91 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 91 insertions(+)
 create mode 100644 test-suite/output/Naming.v

(limited to 'test-suite/output/Naming.v')

diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v
new file mode 100644
index 00000000..327643dc
--- /dev/null
+++ b/test-suite/output/Naming.v
@@ -0,0 +1,91 @@
+(* This file checks the compatibility of naming strategy *)
+(* This does not mean that the given naming strategy is good *)
+
+Parameter x2:nat.
+Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y.
+Section A.
+Variable x3:nat.
+Goal forall x x1 x2 x3:nat,
+  (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3.
+Show.
+intros.
+Show.
+
+(* Remark: in V8.2, this used to be printed
+
+  x3 : nat
+  ============================
+   forall x x1 x4 x5 : nat,
+   (forall x0 x6 : nat, x0 + x1 = x4 + x6) -> x + x1 = x4 + x5
+
+before intro and
+
+  x3 : nat
+  x : nat
+  x1 : nat
+  x4 : nat
+  x0 : nat
+  H : forall x x3 : nat, x + x1 = x4 + x3
+  ============================
+   x + x1 = x4 + x0
+
+after. From V8.3, the quantified hypotheses are printed the sames as
+they would be intro. However the hypothesis H remains printed
+differently to avoid using the same name in autonomous but nested
+subterms *)
+
+Abort.
+
+Goal forall x x1 x2 x3:nat,
+  (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) ->
+   x+x1 = x2+x3 -> foo (S x).
+Show.
+unfold foo.
+Show.
+do 4 intro. (* --> x, x1, x4, x0, ... *)
+Show.
+do 2 intro.
+Show.
+do 4 intro.
+Show.
+
+(* Remark: in V8.2, this used to be printed
+
+  x3 : nat
+  ============================
+   forall x x1 x4 x5 : nat,
+   (forall x0 x6 : nat,
+    x0 + x1 = x4 + x6 ->
+    forall x7 x8 x9 S0 : nat, x7 + S0 = x8 + x9 + (S x0 + x1)) ->
+   x + x1 = x4 + x5 -> forall x0 x6 x7 S0 : nat, x0 + S0 = x6 + x7 + S x
+
+before the intros and
+
+  x3 : nat
+  x : nat
+  x1 : nat
+  x4 : nat
+  x0 : nat
+  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
+  x7 : nat
+  S : nat
+  ============================
+   x5 + S = x6 + x7 + Datatypes.S x
+
+after (note the x5/x0 and the S0/S) *)
+
+Abort.
+
+(* Check naming in hypotheses *)
+
+Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0.
+intros.
+Show.
+apply H with (a:=a). (* test compliance with printing *)
+Abort.
+
-- 
cgit v1.2.3