Fix compilation of horrible Ltac2 example.

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.