Library Coq.Init.Ltac
Export
Set
Default
Proof
Mode
"Classic".