The Coq mailing list

[Eric Tanter <etanter AT dcc.uchile.cl>]

Thanks Ben and Alexandre for the solution and the tip. 
That will certainly be very helpful in the future!

-- Éric


On Dec 26, 2010, at 10:29 AM, Alexandre Pilkiewicz wrote:

> 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
>