From 0f72b089de52ad7d26d71e56003b140fa5012635 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 28 Jul 2017 17:53:42 +0200
Subject: Exporting more internals from Coq implementation.

---
 tests/stuff/ltac2.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'tests/stuff')

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
-- 
cgit v1.2.3