coqbot

Comment author: @fpottier Created attachment 334 Five Coq files that reproduce the problem. Dear Coq authors, I have found a situation where Qed seems to diverge. I have two lemmas...

Comment author: @herbelin Created attachment 336 Version that compiles > Attached file: [HaMLet2.v](https://coq.inria.fr/bugfiles/attachment.cgi?id=336) (text/x-verilog, 14513 bytes) > Description: Version that compiles

Comment author: @herbelin Hi François, It is difficult to say if there really is a loop or simply a very very long computation. With "Lemma ... with ...", you should...

Comment author: @ezyang The following program demonstrates a situation where 'apply' does not manage to unify two terms together, but exact can manage it: (**) Definition transport : forall {A...

Comment author: @ezyang *** Bug [BZ#3103](https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%233103%22) has been marked as a duplicate of this bug. ***

Comment author: @ppedrot Why don't you use a Hint Extern? Hint Extern 0 => exact (@ transport_forall_constant _ _ _ _ _ _ _ _).

Comment author: @ezyang The primary motivation for using auto in the first place is speed. We haven't run any benchmarks, but ostensibly calling back to Ltac can't be the fastest.

Comment author: @JasonGross Another motivation is convenience; it would be nice to be able to write [Hint Exact (@ lem1 _ _ _) (@ lem2 _ _) (@ lem3 _...

Comment author: @JasonGross Perhaps an even more useful command would be something like [Hint Approx lem1 : db.], which would be equivalent to Hint Extern 0 => exact (@ lem1)...

Comment author: @ppedrot Unifying unifications _is_ on the todo-list of the arcane coqdevs, even though I don't expect it to happen before the end of the world as we know...