diff --git a/_CoqProject b/_CoqProject index b47c82cf54505c93b5b5c5e1565ff03b5b5e6adf..fbd492264bbf37a2bae7ebd227db0580c39141f7 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 6b5d01b87c38ccb68dc8ed48cc178985337839c5..9397c0b96648b9e424a4c3025fe895bb11c90dd8 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.