diff options
Diffstat (limited to 'test-suite/ltac2/rebind.v')
| -rw-r--r-- | test-suite/ltac2/rebind.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/test-suite/ltac2/rebind.v b/test-suite/ltac2/rebind.v index 7b3a460c8c..9108871e28 100644 --- a/test-suite/ltac2/rebind.v +++ b/test-suite/ltac2/rebind.v @@ -26,12 +26,10 @@ Ltac2 rec nat_eq n m := | S n => match m with | O => false | S m => nat_eq n m end end. -Ltac2 Type exn ::= [ Assertion_failed ]. - Ltac2 assert_eq n m := match nat_eq n m with | true => () - | false => Control.throw Assertion_failed end. + | false => Control.throw Assertion_failure end. Ltac2 mutable x := O. Ltac2 y := x. |