refactoring

rems-project · Aug 2, 2023 · 567da2f · 567da2f
1 parent ca875af
commit 567da2f
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/coq/CheriMemory/CheriMemory.v b/coq/CheriMemory/CheriMemory.v
@@ -1114,12 +1114,6 @@ Module CheriMemory
     | PV prov ptrval => (prov,ptrval)
     end.
 
-  (** Helper function to split a list at given position.
-      List.split_at in Lem.
-   *)
-  Definition split_at {A:Type} (n:nat) (l:list A)
-    := (List.firstn n l, List.skipn n l).
-
   Inductive overlap_ind :=
   | NoAlloc: overlap_ind
   | SingleAlloc: storage_instance_id -> overlap_ind

diff --git a/coq/Common/Utils.v b/coq/Common/Utils.v
@@ -294,3 +294,9 @@ Proof.
   rewrite H0, H1.
   apply string_eq_refl.
 Qed.
+
+(** Helper function to split a list at given position.
+      List.split_at in Lem.
+ *)
+Definition split_at {A:Type} (n:nat) (l:list A)
+  := (List.firstn n l, List.skipn n l).