Error in pull request

Stream: general

[Sara Díaz Real]

Hello! I have tried to make a pull request and I have found this problem:x-special/nautilus-clipboard
copy
Captura-de-pantalla-de-2021-07-15-20-30-24.png

Can someone help me?

[Bryan Gin-ge Chen]

Sure! If you click on the "Files changed" tab, you'll see a popup which points out the error: "Files in mathlib cannot import the entire tactic folder". So you should see if you can import just the tactics that you use.

[Bryan Gin-ge Chen]

It looks to me like replacing the import tactic line with

import tactic.linarith
import tactic.ring

may work. I've added this as a suggestion on your PR.

[Sara Díaz Real]

Oh, thank you very much! I have accepted your suggestion. It looks like that it is ok. I hope so. Thanks very much, again