Top

Module mathcomp.boot.ssreflect

From Corelib Require Export ssreflect.
Global Set Asymmetric Patterns.
#[warning="-unknown-option,-deprecated-since-9.3"]
Global Set Asymmetric Patterns No Implicits.
Global Set Bullet Behavior "None".

#[deprecated(since="mathcomp 2.3.0", note="Use `Arguments def : simpl never` instead (should work fine since Coq 8.18).")]
Notation nosimpl t := (nosimpl t).

Definition hide {T} t : T := t.
Notation hideT := (@hide (hide _)) (only parsing).
Notation "<hidden >" := (hide _)
  (at level 0, format "<hidden >", only printing) : ssr_scope.

Notation "'[' 'hide' ']'" := (ltac:(
  move; lazymatch goal with
    | |- forall x : ?A, ?G => change (forall x : hide A, G)
    | |- let x : ?A := ?a in ?G => change (let x : hide A := @hide A a in G)
    | _ => fail "[hide] : no top assumption"
  end)) (at level 0, only parsing) : ssripat_scope.

Notation "'[' 'let' ']'" := (ltac:(
  move; lazymatch goal with
    | |- forall (H : let x : ?A := ?a in ?T), ?G =>
      change (let x : A := a in forall H : T, G)
    | |- let H : (let x : ?A := ?a in ?T) := ?t in ?G =>
      change (let x : A := a in let H : T := t in G)
    | |- let H : ?T := (let x : ?A := ?a in ?t) in ?G =>
      change (let x : A := a in let H : T := t in G)
    | _ => fail "[let]: top assumption type or body is not a 'let'"
  end)) (at level 0, only parsing) : ssripat_scope.

Notation "'[' 'fix' ']'" := (ltac:(
  match goal with
  | |- context [?t] =>
    is_fix t; let f := fresh "fix" in set f := t; move: @f => /[hide]
  | _ => fail 1 "[fix]: no visible 'fix' in goal"
  end)) (at level 0, only parsing) : ssripat_scope.

Notation "'[' 'cofix' ']'" := (ltac:(
  match goal with
  | |- context [?t] =>
    is_cofix t; let z := fresh "cofix" in set z := t; move: @z => /[hide]
  | _ => fail 1 "[cofix]: no visible 'cofix' in goal"
  end)) (at level 0, only parsing) : ssripat_scope.