diff options
| author | Pierre-Marie Pédrot | 2017-07-24 19:00:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-24 23:50:58 +0200 |
| commit | 41cea8603b35a1af405650d8a2b9aaa89a445367 (patch) | |
| tree | c41d47f9f5582bb0b267e2422195f8206eb7fef2 /tests | |
| parent | fbfe239730bd5069026ae4e5356e93d3f3bfcb53 (diff) | |
Adding a few primitive functions.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/ltac2.v | 12 |
1 files changed, 12 insertions, 0 deletions
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. |