diff options
| author | Pierre-Marie Pédrot | 2021-03-18 22:21:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-18 22:23:44 +0100 |
| commit | b809bf80bed06303f3d5aa2297787782a030f037 (patch) | |
| tree | d36666d59244fec29e968d3b0e2cd90efe94ea0a /test-suite | |
| parent | eeef63b0b09cf90f7a3022ce6f0d7e50a908484c (diff) | |
Implement ! goal selector for Ltac2.
Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13960.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13960.v b/test-suite/bugs/closed/bug_13960.v new file mode 100644 index 0000000000..947db9586f --- /dev/null +++ b/test-suite/bugs/closed/bug_13960.v @@ -0,0 +1,10 @@ +Require Ltac2.Ltac2. + +Set Default Goal Selector "!". + +Ltac2 t () := let _ := Message.print (Message.of_string "hi") in 42. + +Goal False. +Proof. +Ltac2 Eval t (). +Abort. |