Library Coq.Init.Ltac



#[export] Set Default Proof Mode "Classic".