The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

Is the name of the hypothesis significant, or will it match any hypothesis with that form?

  It will match regardless of the name.

 

Is the number 3 important?

  It is the cost of applying this hint. Auto will try applying "cheaper" hints first.

 

I can apply this tactic directly in the proof and it does work. So clearly matching the hypothesis isn't the problem. Perhaps the crush tactic isn't using the hint? I'm not sure how to check that.

  Note that auto must solve the goal completely or else it will not change the goal in any way. When you apply this tactic directly does it solve the goal completely? Or just "work" giving a new obligation? Can this new obligation be solved by auto?

  Another possibility is that auto only searches the tree up to a given depth: 5 by default, but you can specify it with 'auto n' (n being the depth).

  Hard to say more without a context.

  Best,

  Adam

-- 
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]