blob: de9b9975904e6b8e41bc8fe3cc09467989322df0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Testing the reordering of hypothesis required by pattern, fold and change. *)
Goal forall (A:Set) (x:A) (A':=A), True.
intros.
fold A' in x. (* suceeds: x is moved after A' *)
Undo.
pattern A' in x.
Undo.
change A' in x.
Abort.
(* p and m should be moved before H *)
Goal forall n:nat, n=n -> forall m:nat, let p := (m,n) in True.
intros.
change n with (snd p) in H.
Abort.
|
