From c78af970e1f003587fba9bebdf3ab5ca3b23face Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 30 Sep 2016 12:16:01 +0200
Subject: Fix test-suite.

Restore subst output test file modified by mistake.
---
 test-suite/output/subst.out | 208 --------------------------------------------
 test-suite/output/subst.v   |  11 ---
 2 files changed, 219 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out
index dbb9e09a4..209b2bc26 100644
--- a/test-suite/output/subst.out
+++ b/test-suite/output/subst.out
@@ -26,19 +26,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -52,45 +39,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  H3 : 0 = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
   H1 : 0 = 1
   HA : True
   H2 : 0 = 2
@@ -101,58 +49,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  H3 : 0 = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  H1 : 0 = 1
-  HA : True
-  H2 : 0 = 2
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  ============================
-  True
-1 subgoal
-  
   y, z : nat
   Hy : y = 0
   Hz : z = 0
@@ -179,19 +75,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
   x, y : nat
   Hx : x = 0
   Hy : y = 0
@@ -205,45 +88,6 @@
   True
 1 subgoal
   
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  HB : True
-  H4 : z = 4
-  H3 : 0 = 3
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
   HA, HB : True
   H4 : 0 = 4
   H3 : 0 = 3
@@ -251,55 +95,3 @@
   H2 : 0 = 2
   ============================
   True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
-1 subgoal
-  
-  x, z : nat
-  Hx : x = 0
-  Hz : z = 0
-  H1 : x = 1
-  HA : True
-  H2 : x = 2
-  HB : True
-  H4 : z = 4
-  H3 : 0 = 3
-  ============================
-  True
-1 subgoal
-  
-  y, z : nat
-  Hy : y = 0
-  Hz : z = 0
-  HA : True
-  H3 : y = 3
-  HB : True
-  H4 : z = 4
-  H1 : 0 = 1
-  H2 : 0 = 2
-  ============================
-  True
diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v
index 91bdd03e0..e48aa6bb2 100644
--- a/test-suite/output/subst.v
+++ b/test-suite/output/subst.v
@@ -45,15 +45,4 @@ Show.
 trivial.
 Qed.
 
-(* A bug revealed by OCaml 4.03 warnings *)
-Goal forall y, let x:=0 in y=x -> y=y.
-intros * H;
-subst.
-Fail clear H. (* Was working *)
-Abort.
 
-Goal forall y, let x:=0 in y=x -> y=y.
-intros * H;
-subst.
-Fail clear H. (* Was failing before fix *)
-Abort.
-- 
cgit v1.2.3