Skip to content

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.