The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

I am trying to use Declare Implicit Tactic.

It does not seem to work in my example, the corn division for real numbers.
So, I tried the example from the reference manual.

Parameter quo : nat -> forall n:nat, n<>O -> nat.
Notation "x // y" := (quo x y _) (at level 40).
(* Declare Implicit Tactic assumption.*)
Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
intros. exists (n//m).

As you can see the "Declare Implicit Tactic assumption" does not even seem to be needed. Can someone provide me with a real example?

Thanks,

Bas