The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

On Sun, Mar 25, 2012 at 2:41 PM, henaien amira
<henaien_amira AT hotmail.com>
 wrote:
> Hi everyone,
>
> is there a tactic in Coq that calculate the most general unifier of two
> terms?

Amira, it is well known that in higher order languages, like the base
language of Coq, there's no such most general unifier.

Take as example the following unification problem:

?f y  =  y

where ?f is a meta-variable standing for a function. This problem has 
solutions:
{ (fun x=>x) / ?f } and { (fun x=>y) / ?f }

which are independent.

So, no, there's no such a tactic :-)

Best,
Beta