The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 07/26/2016 06:31 PM, Jonathan Leivent wrote:
> On 07/26/2016 06:23 PM, Robbert Krebbers wrote:
> > Dear Coq club,
> >
> > Could someone explain me the difference between the tactic argument 
> > types uconstr and open_constr?
> >
> > Thanks,
> >
> > Robbert
>
> The differences are (I may be forgetting some):
>
> 1. uconstrs are not type-checked until converted to something else 
> (constr, open_constr) or until type_term is called on them.  Hence it 
> is possible to construct uconstrs that can't possibly type check:
>
> Goal True.
> let X := uconstr:(I I I) in idtac X.
>
> But, one can save time by not type-checking while constructing complex 
> uconstrs.
>
> 2. the holes in uconstrs do not become subgoals until the above type 
> checking occurs, while the holes in open_constrs become subgoals 
> immediately (as the type checking on open_constrs occurs immediately).

Oops - my mistake.  It looks like the holes in uconstrs don't become 
subgoals at all.  Instead, they are either required to be filled or 
inferrable when the uconstr is finally type checked (as by type_term) - 
or, if the uconstr is passed as an open_constr (to a Tactic Notation), 
or to something that acts like an open_constr (like the arg of the 
refine tactic), then the open_constr's rules take over, and subgoals are 
created for holes.  However, each time the same uconstr is passed as an 
open_constr, any holes will create new goals, not drag along the same 
goals (as would happen in the case of an open_constr passed as an 
open_constr).

I guess the way to conceptualize this is that a uconstr is an unchecked 
template for an open_constr.

-- Jonathan

> 3. there is a "uconstr:(..)" form for Ltac, but no corresponding one 
> for open_constr (although one can somewhat get around this via a 
> Tactic Notation).
>
> -- Jonathan