diff options
| author | Jason Gross | 2019-11-27 17:14:51 -0500 |
|---|---|---|
| committer | Jason Gross | 2019-12-06 16:06:35 -0500 |
| commit | 1522090b4cd7a8b7c7e83e316c79bc8c06ab62e9 (patch) | |
| tree | 33ba48a5ebf76a0c248beb4f4dfd42dc0054d299 /test-suite | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
Make the string argument of `time` print correctly
Fixes #10971
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/print_ltac.out | 8 | ||||
| -rw-r--r-- | test-suite/output/print_ltac.v | 12 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out new file mode 100644 index 0000000000..952761acca --- /dev/null +++ b/test-suite/output/print_ltac.out @@ -0,0 +1,8 @@ +Ltac t1 := time "my tactic" idtac +Ltac t2 := let x := string:("my tactic") in + idtac + x +Ltac t3 := idtacstr "my tactic" +Ltac t4 x := match x with + | ?A => (A, A) + end diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v new file mode 100644 index 0000000000..a992846791 --- /dev/null +++ b/test-suite/output/print_ltac.v @@ -0,0 +1,12 @@ +(* Testing of various things about Print Ltac *) +(* https://github.com/coq/coq/issues/10971 *) +Ltac t1 := time "my tactic" idtac. +Print Ltac t1. +Ltac t2 := let x := string:("my tactic") in idtac x. +Print Ltac t2. +Tactic Notation "idtacstr" string(str) := idtac str. +Ltac t3 := idtacstr "my tactic". +Print Ltac t3. +(* https://github.com/coq/coq/issues/9716 *) +Ltac t4 x := match x with ?A => constr:((A, A)) end. +Print Ltac t4. |