Merge pull request #3455 from mtzguido/extractionfix

Extraction.Krml: properly detect mem type, it does not have an argument
FStarLang · Sep 10, 2024 · ef93b7d · ef93b7d
2 parents c7a1cf5 + d1d8633
commit ef93b7d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml
diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst
@@ -660,7 +660,7 @@ let rec translate_type_without_decay' env t: typ =
       TInt (must (mk_width m))
   | MLTY_Named ([], ([ "FStar"; m ], "t'")) when is_machine_int m ->
       TInt (must (mk_width m))
-  | MLTY_Named ([arg], p) when (Syntax.string_of_mlpath p = "FStar.Monotonic.HyperStack.mem") ->
+  | MLTY_Named ([], p) when (Syntax.string_of_mlpath p = "FStar.Monotonic.HyperStack.mem") ->
       TUnit
 
   | MLTY_Named ([_; arg; _], p) when