The Coq mailing list

[Luminous Fennell <mstrlu AT gmx.net>]

Yes that showed it, thanks a lot! It was an issue with coercions.

Lu

On Wed, Jan 18 2012 at 13:23 +0100, Thomas Braibant wrote:

> You should enable the printing of implicit arguments with Set Printing
> All. This is a rule of thumb in this kind of situation, as it usually
> makes it possible to spot why two terms that appear identical are in
> fact different.
>
> With best regards,
> thomas
>
>
>
> On Wed, Jan 18, 2012 at 1:13 PM, Luminous Fennell 
> <mstrlu AT gmx.net>
>  wrote:
>> Hi,
>>
>> At some point in a proof I get this error:
>>
>> Toplevel input, characters 21-90:
>> Error: Impossible to unify
>>  "has_type
>>    (concat empty
>>       (single x (t_arr sec_low (t_unit tsa_dyn) (t_unit sec_high))))
>>    (exp_unit tsa_dyn) (t_unit tsa_dyn)" with
>>  "has_type
>>    (concat empty
>>       (single x (t_arr sec_low (t_unit tsa_dyn) (t_unit sec_high))))
>>    (exp_unit tsa_dyn) (t_unit tsa_dyn)".
>>
>> This seems strange, as the two expressions are identical. I suppose it's
>> a beginner's mistake, but how could this possibly not work? I would very
>> much appreciate any suggestions.
>>
>> I'm using coq 8.3pl2-3 and ProofGeneral 4.1-1.
>>
>> Thanks and best regards
>>
>> Lu