From 41cea8603b35a1af405650d8a2b9aaa89a445367 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 19:00:29 +0200
Subject: Adding a few primitive functions.

---
 tests/ltac2.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'tests')

diff --git a/tests/ltac2.v b/tests/ltac2.v
index 3d3d0032c5..770d385406 100644
--- a/tests/ltac2.v
+++ b/tests/ltac2.v
@@ -117,3 +117,15 @@ Goal True.
 Proof.
 refine! I.
 Abort.
+
+Goal True.
+Proof.
+let x _ := plus (fun _ => 0) (fun _ => 1) in
+match case x with
+| Val x =>
+  match x with
+  | (x, k) => Message.print (Message.of_int (k Not_found))
+  end
+| Err x => Message.print (Message.of_string "Err")
+end.
+Abort.
-- 
cgit v1.2.3