The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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).

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