Library Coq.Init.Ltac



Export Set Default Proof Mode "Classic".