Move `iris.prelude.prelude` to stdpp
It's useful to load stdpp and ssreflect together even when not depending on Iris.
(* Load both ssreflect and stdpp, using the same settings as Iris. *)
From Coq.ssr Require Export ssreflect.
From stdpp Require Export prelude.
#[global] Open Scope general_if_scope.
#[global] Set SsrOldRewriteGoalsOrder. (* See Coq issue #5706 *)
Ltac done := stdpp.tactics.done.
That could be called e.g. stdpp.ssreflect
.
That leaves two other global settings in iris.prelude.prelude
, but:
-
!437 (closed) could handle
Equiv
's mode - The
Z.of_nat
coercion is legacy so it can stay in iris.