From 3978d7f6082b78a2973ea1a5fc8d9ab66dc41737 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Tue, 27 Aug 2024 19:23:38 +0200
Subject: [PATCH] chore: update F*

---
 flake.lock                             | 6 +++---
 fstar/common/proofs/MLS.MiscLemmas.fst | 6 +++++-
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/flake.lock b/flake.lock
index 9782db5..a9d58fe 100644
--- a/flake.lock
+++ b/flake.lock
@@ -72,11 +72,11 @@
         "nixpkgs": "nixpkgs"
       },
       "locked": {
-        "lastModified": 1724479024,
-        "narHash": "sha256-i/RCT2fQzPMM1JOohhPOHzgoURmvUd3HLxGJn+qfnr4=",
+        "lastModified": 1724778396,
+        "narHash": "sha256-qCB4uPRJyxtjYQ9eJob0mWSxjz2A+Eg0ujsCuTBKx8k=",
         "owner": "FStarLang",
         "repo": "FStar",
-        "rev": "eb4ba2057bef600d4c0f4255966af668e8f47d4d",
+        "rev": "8b8de3fffccfa756e4ce3632aa00932ccb9999d7",
         "type": "github"
       },
       "original": {
diff --git a/fstar/common/proofs/MLS.MiscLemmas.fst b/fstar/common/proofs/MLS.MiscLemmas.fst
index d9d0918..2320d2c 100644
--- a/fstar/common/proofs/MLS.MiscLemmas.fst
+++ b/fstar/common/proofs/MLS.MiscLemmas.fst
@@ -139,7 +139,11 @@ val sorted_append:
 let rec sorted_append #a lt cutoff l1 l2 =
   match l1 with
   | [] -> ()
-  | [h] -> ()
+  | [h] -> (
+    match l2 with
+    | [] -> ()
+    | _::_ -> ()
+  )
   | h::t -> sorted_append lt cutoff t l2
 #pop-options