diff options
| -rw-r--r-- | tests/stuff/ltac2.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v index 95bff7e569..370bc70d15 100644 --- a/tests/stuff/ltac2.v +++ b/tests/stuff/ltac2.v @@ -129,7 +129,7 @@ Abort. Goal (forall n : nat, n = 0 -> False) -> True. Proof. refine (fun () => '(fun H => _)). -Std.ecase (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]). +Std.case true (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]). refine (fun () => 'eq_refl). Qed. @@ -138,5 +138,6 @@ Proof. refine (fun () => '(fun x => _)). Std.cbv { Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true; - Std.rZeta := true; Std.rDelta := false; Std.rConst := []; + Std.rZeta := true; Std.rDelta := true; Std.rConst := []; } { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }. +Abort. |