diff options
| author | Pierre-Marie Pédrot | 2020-03-11 10:02:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-11 10:02:17 +0100 |
| commit | 45e83041ee129a541fdf17a8c50dd6e9e0e81262 (patch) | |
| tree | 27ce0770df7c30aca0225ce5a9fbff02b508b288 /tactics/auto.ml | |
| parent | baae1974d5ee15233cddffa1281d4a23fc74cc9f (diff) | |
| parent | 15eb6b5721aaff1281f1f71e00c98fd9a39511e0 (diff) | |
Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constants
Reviewed-by: ppedrot
Diffstat (limited to 'tactics/auto.ml')
0 files changed, 0 insertions, 0 deletions