| IdTac of loc
| Injection of loc * 'term
| Intros of loc * int option * 'ident list
- | LApply of loc * 'term option * 'term
+ | LApply of loc * 'term option * 'term * 'ident option
| Left of loc
| LetIn of loc * 'term * 'ident
| Reduce of loc * reduction_kind * ('term, 'ident) pattern
type ('term,'obj) command =
| Set of loc * string * string
+ | Drop of loc
| Qed of loc
(** name.
* Name is needed when theorem was started without providing a name