From dd4be284c868a437c36cf31c6f19848bbe0a1367 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 29 Nov 2023 16:51:01 -0800 Subject: [PATCH] snap --- ocaml/fstar-lib/generated/FStar_PartialMap.ml | 2 +- ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml | 10 ---------- 2 files changed, 1 insertion(+), 11 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_PartialMap.ml b/ocaml/fstar-lib/generated/FStar_PartialMap.ml index e874ba53c4e..7213a008035 100644 --- a/ocaml/fstar-lib/generated/FStar_PartialMap.ml +++ b/ocaml/fstar-lib/generated/FStar_PartialMap.ml @@ -16,7 +16,7 @@ let upd : 'k 'v . ('k, 'v) t -> 'k -> 'v -> ('k, 'v) t = fun y -> FStar_FunctionalExtensionality.on_domain (fun x1 -> if x1 = x then FStar_Pervasives_Native.Some y else m x1) -let remove : 'k 'v . ('k, 'v) t -> 'k -> ('k, 'v) t = +let remove : 'k 'uuuuu . ('k, 'uuuuu) t -> 'k -> ('k, 'uuuuu) t = fun m -> fun x -> FStar_FunctionalExtensionality.on_domain diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index 38a5671a6f9..446b5fd99c8 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -3,16 +3,6 @@ exception SplitQueryAndRetry let (uu___is_SplitQueryAndRetry : Prims.exn -> Prims.bool) = fun projectee -> match projectee with | SplitQueryAndRetry -> true | uu___ -> false -let (z3_replay_result : (unit * unit)) = ((), ()) -let z3_result_as_replay_result : - 'uuuuu 'uuuuu1 'uuuuu2 . - ('uuuuu, ('uuuuu1 * 'uuuuu2)) FStar_Pervasives.either -> - ('uuuuu, 'uuuuu1) FStar_Pervasives.either - = - fun uu___ -> - match uu___ with - | FStar_Pervasives.Inl l -> FStar_Pervasives.Inl l - | FStar_Pervasives.Inr (r, uu___1) -> FStar_Pervasives.Inr r let (recorded_hints : FStar_Compiler_Hints.hints FStar_Pervasives_Native.option FStar_Compiler_Effect.ref)