From 8dda0c760ca1056bceccec481402c6e279865acf Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Wed, 22 May 2024 17:00:15 -0400 Subject: [PATCH] Remove depedence on axioms for PER lemmas (#89) --- theories/Core/Semantic/PER/Lemmas.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Core/Semantic/PER/Lemmas.v b/theories/Core/Semantic/PER/Lemmas.v index 5fcbb9ef..fd017968 100644 --- a/theories/Core/Semantic/PER/Lemmas.v +++ b/theories/Core/Semantic/PER/Lemmas.v @@ -1,6 +1,6 @@ From Coq Require Import Lia Morphisms Morphisms_Prop Morphisms_Relations PeanoNat Relation_Definitions RelationClasses. From Equations Require Import Equations. -From Mcltt Require Import Axioms Base LibTactics. +From Mcltt Require Import Base LibTactics. From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback. Import Domain_Notations.