diff options
| author | Pierre-Marie Pédrot | 2017-09-01 00:19:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-01 00:19:33 +0200 |
| commit | 2a0a48834f0b90319e56ae9f4a172fe6855583c0 (patch) | |
| tree | 10f7d831e2e2ef8923085f816f7431edf4cd1a7b /tests/errors.v | |
| parent | 72e3d2e563e08627559065ff0289403591d99682 (diff) | |
Passing an optional message to Tactic_failure.
Diffstat (limited to 'tests/errors.v')
| -rw-r--r-- | tests/errors.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/errors.v b/tests/errors.v index e7beff3420..c677f6af5d 100644 --- a/tests/errors.v +++ b/tests/errors.v @@ -7,6 +7,6 @@ let x := Control.plus (fun e => match e with Not_found => 1 | _ => 2 end) in match Int.equal x 2 with | true => () -| false => Control.throw Tactic_failure +| false => Control.throw (Tactic_failure None) end. Abort. |