The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

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