From af1c10475f3ce28fd471ca3b94d126f7f892b213 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 10 Aug 2022 15:14:18 +0200 Subject: [PATCH] =?UTF-8?q?Rename=20`frame=5Finstances`=20=E2=86=92=20`cla?= =?UTF-8?q?ss=5Finstances=5Fframe`.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- _CoqProject | 2 +- iris/proofmode/{frame_instances.v => class_instances_frame.v} | 0 iris/proofmode/proofmode.v | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) rename iris/proofmode/{frame_instances.v => class_instances_frame.v} (100%) diff --git a/_CoqProject b/_CoqProject index b47c82cf5..fbd492264 100644 --- a/_CoqProject +++ b/_CoqProject @@ -140,7 +140,7 @@ iris/proofmode/class_instances_updates.v iris/proofmode/class_instances_embedding.v iris/proofmode/class_instances_plainly.v iris/proofmode/class_instances_internal_eq.v -iris/proofmode/frame_instances.v +iris/proofmode/class_instances_frame.v iris/proofmode/monpred.v iris/proofmode/modalities.v iris/proofmode/modality_instances.v diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/class_instances_frame.v similarity index 100% rename from iris/proofmode/frame_instances.v rename to iris/proofmode/class_instances_frame.v diff --git a/iris/proofmode/proofmode.v b/iris/proofmode/proofmode.v index 6b5d01b87..9397c0b96 100644 --- a/iris/proofmode/proofmode.v +++ b/iris/proofmode/proofmode.v @@ -7,5 +7,5 @@ these files. *) From iris.proofmode Require Import class_instances class_instances_later class_instances_updates class_instances_embedding class_instances_plainly class_instances_internal_eq. -From iris.proofmode Require Import frame_instances modality_instances. +From iris.proofmode Require Import class_instances_frame modality_instances. From iris.prelude Require Import options. -- GitLab