Library Ltac2.Float

Require Import Ltac2.Init.

Ltac2 Type t := float.

Ltac2 @ external equal : t -> t -> bool := "rocq-runtime.plugins.ltac2" "float_equal".