D.prelude
(* Base Coq settings (ssreflect and setup): *)
From Coq.Program Require Export Equality.
From Coq Require ProofIrrelevance.
From iris.prelude Require Export prelude.
From Autosubst Require Export Autosubst.
From D Require Export tactics.
From iris.program_logic Require Import language.
#[global] Set Suggest Proof Using.
#[global] Set Default Proof Using "Type".
From Coq.Program Require Export Equality.
From Coq Require ProofIrrelevance.
From iris.prelude Require Export prelude.
From Autosubst Require Export Autosubst.
From D Require Export tactics.
From iris.program_logic Require Import language.
#[global] Set Suggest Proof Using.
#[global] Set Default Proof Using "Type".
Workaround https://github.com/coq/coq/issues/4230. Taken from Software Foundations.
#[global] Remove Hints Bool.trans_eq_bool : core.
https://github.com/math-comp/analysis/blob/bb4938c2dee89e91668f8d6a251e968d2f5a05ae/theories/posnum.vL51-L52 Enrico (Tassi?)'s trick for tc resolution in have. Doesn't conflict with infix !!.
Notation "!! x" := (ltac:(refine x)) (at level 100, only parsing).
Notation Reduce tm := ltac:(let res := eval red in tm in exact res) (only parsing).
Notation Unfold def tm := ltac:(let res := eval unfold def in tm in exact res) (only parsing).
Definition disable_tc_search {T : Type} (x : id T) : T := x.
Notation notc_hole := (disable_tc_search _).
(*
If prelude and Program are imported after Iris modules,
side effects from iris.algebra.base and stdpp.base, including
setting the obligation tactic, won't be re-run. So let's do it
ourselves: *)
#[global] Obligation Tactic := idtac.
Notation Reduce tm := ltac:(let res := eval red in tm in exact res) (only parsing).
Notation Unfold def tm := ltac:(let res := eval unfold def in tm in exact res) (only parsing).
Definition disable_tc_search {T : Type} (x : id T) : T := x.
Notation notc_hole := (disable_tc_search _).
(*
If prelude and Program are imported after Iris modules,
side effects from iris.algebra.base and stdpp.base, including
setting the obligation tactic, won't be re-run. So let's do it
ourselves: *)
#[global] Obligation Tactic := idtac.
Autosubst extensions: notations
Notation shiftN n chi := chi.|[ren (+n)].
Notation shiftVN n v := v.[ren (+n)].
(* Define these afterwards, so they're used in preference when printing *)
Notation shift chi := (shiftN 1 chi).
Notation shiftV v := (shiftVN 1 v).
Notation shiftVN n v := v.[ren (+n)].
(* Define these afterwards, so they're used in preference when printing *)
Notation shift chi := (shiftN 1 chi).
Notation shiftV v := (shiftVN 1 v).
Definition mapsnd {A} `(f : B → C) : A × B → A × C := λ '(a, b), (a, f b).
Definition stamp := positive.
Definition stamp := positive.
Call red on each hypothesis at most once.
Not defined in tactics.v because it uses stdpp.
Ltac red_hyps_once :=
repeat_on_hyps (fun H ⇒ try_once_tac H (red in H)); un_usedLemma.
repeat_on_hyps (fun H ⇒ try_once_tac H (red in H)); un_usedLemma.