The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

2010/12/26 Ben Moseley 
<ben_moseley AT mac.com>:
> The problem seems to be that the two different usages of '+' in your 
> 'assert' are getting mapped to different 'plus' implementations.
>
> This can be seen if you use:
>
> Unset Printing Notations.
>
>  assert (H: S (S n') + m = S (S (n' + m))).
>
> ...
>
>   eq (plus (S (S n')) m) (S (S (Peano.plus n' m)))

I would like to add that in general, when you have this kind of weird
error message:
'Found no subterm matching "foo" in the current goal.' when you do see
a "foo" in your goal
or "Cannot unify foo with foo", the first thing to do is : Set Printing All.
In your example the problem was due to a notation. It is often the
case that an implicit argument is not the same on both side (an alias
could have been chosen). Set Printing All removes all use of notation,
implicit argument, etc, and allows you to quickly spot the real
problem.

Hope this helps for the future

Alexandre