diff options
| author | Gaëtan Gilbert | 2020-02-06 15:39:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 3faf22b382379f08d5a918bd535287f57e2fc0fc (patch) | |
| tree | 86c9800550b752396a4532c23b3120118dc3bdb0 /plugins | |
| parent | e12cfbafbce3a1c6719d7e4d34fe64a81cce90b2 (diff) | |
unsafe_type_of -> get_type_of in Tactics.atomize_param_of_ind_then
Not 100% sure about this one TBH, this function is messy.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions