Library Corelib.Init.Ltac



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

Forward declaration for ltac2.
Ltac easy_forward_decl := fail "Cannot use easy: Corelib.Init.Tactics not loaded".