The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Jan 21, 2015 at 07:32:28PM +0100, Ali Assaf wrote:
> Hi,
> 
> The description of Matita's kernel implementation in "A compact kernel
> for the calculus of inductive constructions" contains a type system in
> the appendix that includes metavariables, although it is not
> commented.

That type system is the one for the kernel.  Metavariables are pretty
much like constants, they have a type declared in a dedicated
environment and they are only equal to themselves.

Things get interesting when the conversion test is allowed to
instantiate them in order to succeed.  In this case is more correct to
call the conversion test higher order unification.  This algorithm is
not properly documented in such paper, and not in any other paper about
Matita.  Eventually it will be...

Best,
-- 
Enrico Tassi