Skip to content
Snippets Groups Projects
Commit af1c1047 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename `frame_instances` → `class_instances_frame`.

parent abefed6c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 1
− 1
View file @ af1c1047
...@@ -140,7 +140,7 @@ iris/proofmode/class_instances_updates.v ...@@ -140,7 +140,7 @@ iris/proofmode/class_instances_updates.v
iris/proofmode/class_instances_embedding.v iris/proofmode/class_instances_embedding.v
iris/proofmode/class_instances_plainly.v iris/proofmode/class_instances_plainly.v
iris/proofmode/class_instances_internal_eq.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/monpred.v
iris/proofmode/modalities.v iris/proofmode/modalities.v
iris/proofmode/modality_instances.v iris/proofmode/modality_instances.v
......
iris/proofmode/proofmode.v
+ 1
− 1
View file @ af1c1047
...@@ -7,5 +7,5 @@ these files. *) ...@@ -7,5 +7,5 @@ these files. *)
From iris.proofmode Require Import class_instances class_instances_later From iris.proofmode Require Import class_instances class_instances_later
class_instances_updates class_instances_embedding class_instances_updates class_instances_embedding
class_instances_plainly class_instances_internal_eq. 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. From iris.prelude Require Import options.
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