The Coq mailing list

[Tej Chajed <tchajed AT mit.edu>]

Another source of problems is that firstorder by default calls [auto with *] on all goals, using all hint databases, which is far too aggressive (here's a bug report proposing to fix this). In the meantime you can use [Set Firstorder Solver auto] or manually pass firstorder a tactic.

Note that it doesn't matter what hint database the INR_eq theorem is in if you're using firstorder auto with *.

On Fri, Jan 25, 2019 at 7:15 AM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

Hi

it is just that the theorem INR_eq : INR m = INR n -> m = n has wrongly
been put in the hint resolve database of reals.
When you load Psatz you lod this database.

So firstorder automatically lifts your equality to the reals applying
this theorem and then unlift it by f_equal to finally prove it with
omega ;-)

Could you file a bug report at

https://github.com/coq/coq/issues

so we remember to fix this issue.


On 1/25/19 7:14 AM, Caitlin D'Abrera wrote:
> Hi all, 
>
> I have noticed some peculiar behaviour with tactics like firstorder and
> was hoping for an explanation.
>