Auto : last hole does not get filled #193
Description
Most of the time, CornelisAuto does not work on the last hole (while it was previously able to compute a solution of exactly the same form). Could someone guide me to the place where this could get fixed ?
Example (from https://github.com/leo-leesco/hott/blob/main/Equivalence.agda):
pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B
pathToEquiv refl = id , (id , (λ x → refl)) , ?The last ? should be filled with (id , (λ x → refl)), just like the previous argument.
Thanks !