Library Ltac2.Proj

Require Import Ltac2.Init.

Ltac2 Type t := projection.

Ltac2 @ external equal : t -> t -> bool := "ltac2" "projection_equal".