Library zoo.options
From Stdlib.ssr Require Import
ssreflect.
From zoo Require Export
tactics.
#[export] Set Default Proof Using "Type*".
#[export] Set Suggest Proof Using.
#[export] Set Bullet Behavior "Strict Subproofs".
#[export] Unset SsrOldRewriteGoalsOrder.
#[export] Set Printing Projections.
ssreflect.
From zoo Require Export
tactics.
#[export] Set Default Proof Using "Type*".
#[export] Set Suggest Proof Using.
#[export] Set Bullet Behavior "Strict Subproofs".
#[export] Unset SsrOldRewriteGoalsOrder.
#[export] Set Printing Projections.