Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 16 insertions, 12 deletions

diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
index bba356f2..6fd0fe8b 100644
--- a/test-suite/ideal-features/Apply.v
+++ b/test-suite/ideal-features/Apply.v
@@ -6,21 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This needs unification on type *)
+(* This needs step by step unfolding *)
 
-Goal (n,m:nat)(eq nat (S m) (S n)).
-Intros.
-Apply f_equal.
+Fixpoint T (n:nat) : Prop :=
+  match n with
+  | O => True
+  | S p => n = n -> T p
+  end.
 
-(* f_equal : (A,B:Set; f:(A->B); x,y:A)x=y->(f x)=(f y) *)
-(* and A cannot be deduced from the goal but only from the type of f, x or y *)
+Require Import Arith.
 
+Goal T 3 -> T 1.
+intro H.
+apply H.
 
-(* This needs step by step unfolding *)
+(* This needs unification on type *)
 
-Fixpoint T [n:nat] : Prop := Cases n of O => True | (S p) => n=n->(T p) end.
-Require Arith.
+Goal forall n m : nat, S m = S n :>nat.
+intros.
+apply f_equal.
 
-Goal (T (3))->(T (1)).
-Intro H.
-Apply H.
+(* f_equal : forall (A B:Set) (f:A->B) (x y:A), x=y->(f x)=(f y) *)
+(* and A cannot be deduced from the goal but only from the type of f, x or y *)