fix HACL* snapshot

Inria-Prosecco · Jan 8, 2025 · 238a073 · 238a073
1 parent d86faf8
commit 238a073
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/hacl-star-snapshot/haclml/FStar_Range.ml b/hacl-star-snapshot/haclml/FStar_Range.ml
@@ -0,0 +1,7 @@
+open Prims
+(* Following FStarLang/FStar#3637 FStar_Range is reserved for plugins *)
+(* However it is used by the HACL* snapshot for some reason *)
+(* Emulating the minimal interface here *)
+type ('a, 'b, 'c) labeled = unit
+type range = unit
+let mk_range (s:string) (i1:int) (i2:int) (i3:int) (i4:int): range = ()
diff --git a/hacl-star-snapshot/haclml/dune b/hacl-star-snapshot/haclml/dune
@@ -3,7 +3,7 @@
  (public_name mls.haclml)
  (wrapped false)
  (modes byte native)
- (libraries fstar.pluginlib)
+ (libraries fstar.lib)
  (virtual_modules primitives)
  (default_implementation primitives_native)
  (modules (:standard \ Meta_Interface Lib_Buffer Lib_ByteBuffer Lib_Loops)))