diff options
| author | Pierre-Marie Pédrot | 2019-12-18 16:49:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-18 16:49:53 +0100 |
| commit | 6b9f6c365ec5b478e79f70cf2a1ae4faed809b74 (patch) | |
| tree | 057a9b5816b2e202d2fd306849b8beb7f3d3782e | |
| parent | 6fb1b92c1f4a6f25f487107c3f3a89057ba2ee77 (diff) | |
| parent | 1522090b4cd7a8b7c7e83e316c79bc8c06ab62e9 (diff) | |
Merge PR #11203: Make the string argument of `time` print correctly
Ack-by: Zimmi48
Reviewed-by: ppedrot
| -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 12a5c11e5e..b99d2a0d45 100644 --- a/.gitignore +++ b/.gitignore @@ -93,6 +93,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 0e8c225a8f..7843faaef3 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. |