Pulse.Lib.Array.memcpy does not require eqtype

Author: tahina-pro

lib/pulse/lib/Pulse.Lib.Array.fst

@@ -53,7 +53,7 @@ fn compare (#t:eqtype) (l:US.t) (a1 a2:larray t (US.v l)) (#p1 #p2:perm)
   (!i = l)
 }
 
-fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
+fn memcpy_l (#t:Type0) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
            (#p:perm) (#src0 #dst0:Ghost.erased (Seq.seq t))
   requires pts_to src #p src0 **
            pts_to dst dst0
@@ -89,7 +89,7 @@ fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
 
 
 fn memcpy
-  (#t:eqtype)
+  (#t:Type0)
   (l:SZ.t)
   (src dst:larray t (SZ.v l))
   (#p:perm)

lib/pulse/lib/Pulse.Lib.Array.fsti

@@ -41,7 +41,7 @@ fn compare
      pure (res <==> Seq.equal s1 s2)
 
 fn memcpy_l
-        (#t:eqtype)
+        (#t:Type0)
         (l:SZ.t)
         (src dst:(a:array t { SZ.v l <= length a }))
         (#p:perm)
@@ -54,7 +54,7 @@ fn memcpy_l
                                    (Seq.slice dst0 (SZ.v l) (length dst)))
 
 fn memcpy
-        (#t:eqtype)
+        (#t:Type0)
         (l:SZ.t)
         (src dst:larray t (SZ.v l))
         (#p:perm)