Commit 68e1a9ac authored by Michael Sammler's avatar Michael Sammler
Browse files

update imports in lithium base

parent d7b0f050
Pipeline #55246 passed with stage
in 13 minutes and 37 seconds
...@@ -4,9 +4,8 @@ From iris.algebra Require Export big_op. ...@@ -4,9 +4,8 @@ From iris.algebra Require Export big_op.
From Coq.ZArith Require Import Znumtheory. From Coq.ZArith Require Import Znumtheory.
From stdpp Require Import gmap list. From stdpp Require Import gmap list.
From iris.program_logic Require Import weakestpre. From iris.program_logic Require Import weakestpre.
From iris.bi Require Import derived_laws. From iris.bi Require Import bi.
Import interface.bi derived_laws.bi. From iris.proofmode Require Import proofmode.
From iris.proofmode Require Import tactics.
From stdpp Require Import natmap. From stdpp Require Import natmap.
From refinedc.lithium Require Import Z_bitblast. From refinedc.lithium Require Import Z_bitblast.
Set Default Proof Using "Type". Set Default Proof Using "Type".
...@@ -75,7 +74,7 @@ Tactic Notation "reduce_closed" constr(x) := ...@@ -75,7 +74,7 @@ Tactic Notation "reduce_closed" constr(x) :=
(* from https://mattermost.mpi-sws.org/iris/pl/dcktjjjpsiycmrieyh74bzoagr *) (* from https://mattermost.mpi-sws.org/iris/pl/dcktjjjpsiycmrieyh74bzoagr *)
Ltac solve_sep_entails := Ltac solve_sep_entails :=
try (apply equiv_entails; split); try (apply (anti_symm _));
iIntros; iIntros;
repeat iMatchHyp (fun H P => repeat iMatchHyp (fun H P =>
lazymatch P with lazymatch P with
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment