diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index f179ffe38..3518e40c4 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -401,8 +401,9 @@ struct
     let ppat = ppat' false in
     match p.p with
     | PWild -> F.wild
-    | PAscription { typ; pat } ->
+    | PAscription { typ; pat = { p = PBinding _; _ } as pat } ->
         F.pat @@ F.AST.PatAscribed (ppat pat, (pty p.span typ, None))
+    | PAscription { pat; _ } -> ppat pat
     | PBinding
         {
           mut = Immutable;
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index efe3f1ef0..f3bb80621 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -38,7 +38,7 @@ type t_Foo = { f_field:u8 }
 let v_CONSTANT: t_Foo = { f_field = 3uy } <: t_Foo
 
 let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
-  let (_: u64):u64 =
+  let _:u64 =
     ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64)
         <:
         u64) +!
@@ -47,28 +47,28 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
       u64) +!
     (cast (xs <: usize) <: u64)
   in
-  let (_: u32):u32 =
+  let _:u32 =
     ((((cast (x8 <: u8) <: u32) +! (cast (x16 <: u16) <: u32) <: u32) +! x32 <: u32) +!
       (cast (x64 <: u64) <: u32)
       <:
       u32) +!
     (cast (xs <: usize) <: u32)
   in
-  let (_: u16):u16 =
+  let _:u16 =
     ((((cast (x8 <: u8) <: u16) +! x16 <: u16) +! (cast (x32 <: u32) <: u16) <: u16) +!
       (cast (x64 <: u64) <: u16)
       <:
       u16) +!
     (cast (xs <: usize) <: u16)
   in
-  let (_: u8):u8 =
+  let _:u8 =
     (((x8 +! (cast (x16 <: u16) <: u8) <: u8) +! (cast (x32 <: u32) <: u8) <: u8) +!
       (cast (x64 <: u64) <: u8)
       <:
       u8) +!
     (cast (xs <: usize) <: u8)
   in
-  let (_: i64):i64 =
+  let _:i64 =
     ((((cast (x8 <: u8) <: i64) +! (cast (x16 <: u16) <: i64) <: i64) +! (cast (x32 <: u32) <: i64)
         <:
         i64) +!
@@ -77,7 +77,7 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
       i64) +!
     (cast (xs <: usize) <: i64)
   in
-  let (_: i32):i32 =
+  let _:i32 =
     ((((cast (x8 <: u8) <: i32) +! (cast (x16 <: u16) <: i32) <: i32) +! (cast (x32 <: u32) <: i32)
         <:
         i32) +!
@@ -86,7 +86,7 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
       i32) +!
     (cast (xs <: usize) <: i32)
   in
-  let (_: i16):i16 =
+  let _:i16 =
     ((((cast (x8 <: u8) <: i16) +! (cast (x16 <: u16) <: i16) <: i16) +! (cast (x32 <: u32) <: i16)
         <:
         i16) +!
@@ -95,7 +95,7 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
       i16) +!
     (cast (xs <: usize) <: i16)
   in
-  let (_: i8):i8 =
+  let _:i8 =
     ((((cast (x8 <: u8) <: i8) +! (cast (x16 <: u16) <: i8) <: i8) +! (cast (x32 <: u32) <: i8)
         <:
         i8) +!
@@ -115,7 +115,7 @@ let math_integers (x: Hax_lib.Int.t_Int)
     : Prims.Pure u8
       (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
       (fun _ -> Prims.l_True) =
-  let (_: Hax_lib.Int.t_Int):Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in
+  let _:Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in
   let _:bool =
     ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) >
     (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int)
@@ -129,26 +129,26 @@ let math_integers (x: Hax_lib.Int.t_Int)
   let _:Hax_lib.Int.t_Int = x - x in
   let _:Hax_lib.Int.t_Int = x * x in
   let _:Hax_lib.Int.t_Int = x / x in
-  let (_: i16):i16 = Hax_lib.Int.impl__Int__to_i16 x in
-  let (_: i32):i32 = Hax_lib.Int.impl__Int__to_i32 x in
-  let (_: i64):i64 = Hax_lib.Int.impl__Int__to_i64 x in
-  let (_: i128):i128 = Hax_lib.Int.impl__Int__to_i128 x in
-  let (_: isize):isize = Hax_lib.Int.impl__Int__to_isize x in
-  let (_: u16):u16 = Hax_lib.Int.impl__Int__to_u16 x in
-  let (_: u32):u32 = Hax_lib.Int.impl__Int__to_u32 x in
-  let (_: u64):u64 = Hax_lib.Int.impl__Int__to_u64 x in
-  let (_: u128):u128 = Hax_lib.Int.impl__Int__to_u128 x in
-  let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in
+  let _:i16 = Hax_lib.Int.impl__Int__to_i16 x in
+  let _:i32 = Hax_lib.Int.impl__Int__to_i32 x in
+  let _:i64 = Hax_lib.Int.impl__Int__to_i64 x in
+  let _:i128 = Hax_lib.Int.impl__Int__to_i128 x in
+  let _:isize = Hax_lib.Int.impl__Int__to_isize x in
+  let _:u16 = Hax_lib.Int.impl__Int__to_u16 x in
+  let _:u32 = Hax_lib.Int.impl__Int__to_u32 x in
+  let _:u64 = Hax_lib.Int.impl__Int__to_u64 x in
+  let _:u128 = Hax_lib.Int.impl__Int__to_u128 x in
+  let _:usize = Hax_lib.Int.impl__Int__to_usize x in
   Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int)
 
 let null: char = '\0'
 
 let numeric (_: Prims.unit) : Prims.unit =
-  let (_: usize):usize = sz 123 in
-  let (_: isize):isize = isz (-42) in
-  let (_: isize):isize = isz 42 in
-  let (_: i32):i32 = (-42l) in
-  let (_: u128):u128 = pub_u128 22222222222222222222 in
+  let _:usize = sz 123 in
+  let _:isize = isz (-42) in
+  let _:isize = isz 42 in
+  let _:i32 = (-42l) in
+  let _:u128 = pub_u128 22222222222222222222 in
   ()
 
 let patterns (_: Prims.unit) : Prims.unit =
@@ -190,7 +190,7 @@ let panic_with_msg (_: Prims.unit) : Prims.unit =
       Rust_primitives.Hax.t_Never)
 
 let empty_array (_: Prims.unit) : Prims.unit =
-  let (_: t_Slice u8):t_Slice u8 =
+  let _:t_Slice u8 =
     (let list:Prims.list u8 = [] in
       FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 0);
       Rust_primitives.Hax.array_of_list 0 list)
diff --git a/test-harness/src/snapshots/toolchain__patterns into-fstar.snap b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap
new file mode 100644
index 000000000..77025089e
--- /dev/null
+++ b/test-harness/src/snapshots/toolchain__patterns into-fstar.snap	
@@ -0,0 +1,41 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: fstar
+  info:
+    name: patterns
+    manifest: patterns/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: true
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Patterns.fst" = '''
+module Patterns
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Other = | Other : i32 -> t_Other
+
+type t_Test = | Test_C1 : t_Other -> t_Test
+
+let impl__test (self: t_Test) : i32 = match self with | Test_C1 c -> c._0
+'''
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index 5fcbe4dc7..1a2c1f3b8 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -320,7 +320,7 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
 
 [[package]]
 name = "hax-lib"
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 dependencies = [
  "hax-lib-macros",
  "num-bigint",
@@ -329,7 +329,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros"
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 dependencies = [
  "hax-lib-macros-types",
  "paste",
@@ -341,7 +341,7 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-macros-types"
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -352,14 +352,14 @@ dependencies = [
 
 [[package]]
 name = "hax-lib-protocol"
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 dependencies = [
  "libcrux",
 ]
 
 [[package]]
 name = "hax-lib-protocol-macros"
-version = "0.1.0-alpha.1"
+version = "0.1.0-rc.1"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -664,6 +664,10 @@ checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
 name = "pattern-or"
 version = "0.1.0"
 
+[[package]]
+name = "patterns"
+version = "0.1.0"
+
 [[package]]
 name = "ping-pong"
 version = "0.1.0"
diff --git a/tests/Cargo.toml b/tests/Cargo.toml
index df3b03ffa..5e73e647e 100644
--- a/tests/Cargo.toml
+++ b/tests/Cargo.toml
@@ -23,6 +23,7 @@ members = [
         "dyn",
         "reordering",
         "nested-derefs",
+        "patterns",
         "proverif-minimal",
         "proverif-basic-structs",
         "proverif-ping-pong",
diff --git a/tests/patterns/Cargo.toml b/tests/patterns/Cargo.toml
new file mode 100644
index 000000000..f6b4e63d6
--- /dev/null
+++ b/tests/patterns/Cargo.toml
@@ -0,0 +1,9 @@
+[package]
+name = "patterns"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[package.metadata.hax-tests]
+into."fstar" = { issue_id = "1170" }
\ No newline at end of file
diff --git a/tests/patterns/src/lib.rs b/tests/patterns/src/lib.rs
new file mode 100644
index 000000000..058e37b70
--- /dev/null
+++ b/tests/patterns/src/lib.rs
@@ -0,0 +1,15 @@
+#![allow(dead_code)]
+
+struct Other<'a>(&'a i32);
+
+enum Test<'a> {
+    C1(Other<'a>),
+}
+
+impl<'a> Test<'a> {
+    fn test(&self) -> i32 {
+        match self {
+            Self::C1(c) => *c.0,
+        }
+    }
+}