Library iris.proofmode.reduction

From Require Import bi telescopes.
From iris.proofmode Require Import base environments.
From iris.prelude Require Import options.

Called by all tactics to perform computation to lookup items in the context. We avoid reducing anything user-visible here to make sure we do not reduce e.g. before unification happens in iApply. This needs to contain all definitions used in the user-visible statements in coq_tactics, and their dependencies.
Called by many tactics for redexes that are created by instantiation. This cannot create any envs redexes so we just do the cbn part.
Declare Reduction pm_prettify := cbn [
  tele_fold tele_bind tele_app
  bi_persistently_if bi_affinely_if bi_absorbingly_if bi_intuitionistically_if
  bi_wandM bi_laterN
  bi_tforall bi_texist
Ltac pm_prettify :=
  match goal with |- ?ulet v := eval pm_prettify in u in change_no_check v end.