blob: 25ee81b587cfba86c5cf93b2794fb4d6d73cc8fa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
(* Test various subtleties of the "subst" tactics *)
(* Should proceed from left to right (see #4222) *)
Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y.
intros.
subst.
change (3 = 2) in H1.
change (3 = 3).
Abort.
(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *)
Goal forall x y, x = y -> x = 3 -> x = y.
intros.
subst.
change (3 = 3).
Abort.
(* Should substitute cycles once, until a recursive equation is obtained *)
(* (failed in 8.4) *)
Goal forall x y, x = S y -> y = S x -> x = y.
intros.
subst.
change (y = S (S y)) in H0.
change (S y = y).
Abort.
(* A bug revealed by OCaml 4.03 warnings *)
(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *)
Goal forall y, let x:=0 in y=x -> y=y.
intros * H;
(* This worked as expected *)
subst.
Fail clear H.
Abort.
Goal forall y, let x:=0 in x=y -> y=y.
intros * H;
(* Before the fix, this unfolded x instead of
substituting y and erasing H *)
subst.
Fail clear H.
Abort.
|
