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 | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
Make the string argument of `time` print correctly
Fixes #10971
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/11203-fix-time-printing.rst | 4 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/print_ltac.out | 8 | ||||
| -rw-r--r-- | test-suite/output/print_ltac.v | 12 |
5 files changed, 26 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 6c117028a9..7ae2260a86 100644 --- a/.gitignore +++ b/.gitignore @@ -92,6 +92,7 @@ test-suite/coqdoc/Coqdoc.* test-suite/coqdoc/index.html test-suite/coqdoc/coqdoc.css test-suite/output/MExtraction.out +test-suite/output/*.out.real test-suite/oUnit-anon.cache test-suite/unit-tests/**/*.test diff --git a/doc/changelog/04-tactics/11203-fix-time-printing.rst b/doc/changelog/04-tactics/11203-fix-time-printing.rst new file mode 100644 index 0000000000..cdfd2b228e --- /dev/null +++ b/doc/changelog/04-tactics/11203-fix-time-printing.rst @@ -0,0 +1,4 @@ +- The optional string argument to :tacn:`time` is now properly quoted + under :cmd:`Print Ltac` (`#11203 + <https://github.com/coq/coq/pull/11203>`_, fixes `#10971 + <https://github.com/coq/coq/issues/10971>`_, by Jason Gross) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6df068883c..e0b702ba89 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -971,7 +971,7 @@ let pr_goal_selector ~toplevel s = | TacTime (s,t) -> hov 1 ( keyword "time" - ++ pr_opt str s ++ spc () + ++ pr_opt qstring s ++ spc () ++ pr_tac (ltactical,E) t), ltactical | TacRepeat t -> 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. |