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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(* Ensure order of hypotheses is respected after "subst" *)
Set Regular Subst Tactic.
Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
intros * Hx Hy Hz H1 HA H2 H3 HB H4.
(* From now on, the order after subst is consistently H1, HA, H2, H3, HB, H4 *)
subst x.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
Show.
Undo.
subst y.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
Show.
Undo.
subst z.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
Show.
Undo.
subst.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
Show.
trivial.
Qed.
Unset Regular Subst Tactic.
Goal forall x y z, x = 0 -> y = 0 -> z = 0 -> x = 1 -> True -> x = 2 -> y = 3 -> True -> z = 4 -> True.
intros * Hx Hy Hz H1 HA H2 H3 HB H4.
subst x.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, H3, HB, H4, H1, H2 *)
Show.
Undo.
subst y.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, HB, H4, H3 *)
Show.
Undo.
subst z.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was H1, HA, H2, H3, HB, H4 *)
Show.
Undo.
subst.
(* In 8.4 or 8.5 without regular subst tactic mode, the order was HA, HB, H4, H3, H1, H2 *)
(* In 8.5pl0 and 8.5pl1 with regular subst tactic mode, the order was HA, HB, H1, H2, H3, H4 *)
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.
|
