Exporting more internals from Coq implementation.

1 files changed, 7 insertions, 1 deletions

diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index 4950a20ec4..35546ef6c1 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -120,7 +120,6 @@ Abort.
 
 Goal True.
 Proof.
-
 let x () := plus (fun () => 0) (fun _ => 1) in
 match case x with
 | Val x =>
@@ -131,6 +130,13 @@ match case x with
 end.
 Abort.
 
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+refine (fun () => '(fun H => _)).
+Std.ecase (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
+refine (fun () => 'eq_refl).
+Qed.
+
 Ltac2 rec do n tac := match Int.equal n 0 with
 | true => ()
 | false => tac (); do (Int.sub n 1) tac