diff options
| author | Pierre-Marie Pédrot | 2020-11-02 12:58:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-02 12:58:50 +0100 |
| commit | a392b0225a606b6c8fe0051f0d301d5f3b6d5cd3 (patch) | |
| tree | fb5f0abc2db3c2b21c26b20252f3bb5998626864 /lib/pp_diff.ml | |
| parent | 4ab2522244f703f73323ee918bb324cce4b9b237 (diff) | |
| parent | c1e7b28f5977eafd45c36c2ffdca9b7145d867bb (diff) | |
Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" when "foo" is an Ltac
Reviewed-by: ppedrot
Diffstat (limited to 'lib/pp_diff.ml')
0 files changed, 0 insertions, 0 deletions