diff options
| author | Pierre-Marie Pédrot | 2019-12-05 13:32:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-05 13:32:49 +0100 |
| commit | 24936224d5170ba76162ff28eb091be10eace684 (patch) | |
| tree | 15b831f076391605de4d9da142f91c862bd86089 /dev | |
| parent | effbc03b9072ff94f96e54a5026ce04d7aa41bcc (diff) | |
| parent | d9a0cdc557d2c8b94b9fe2f8b78eacf8be4f77f9 (diff) | |
Merge PR #11210: Tacinterp: push_trace doesn't need to be wrapped in a tactic
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions