diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index fdbcd65613feb2647013fb872ef3b99e21bf3f2e..d2c524e2f8ace0751965d78f5201c358d2994051 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -67,10 +67,8 @@ Module StringToIdent.
   does not support returning values from Ltac2 to Ltac1. So we provide
   [string_to_ident_cps] in CPS instead. *)
 
-  Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
-
   Ltac string_to_ident_cps :=
-    ltac2:(s1 r |- let s := get_opt (Ltac1.to_constr s1) in
+    ltac2:(s1 r |- let s := Option.get (Ltac1.to_constr s1) in
                    let ident := coq_string_to_ident s in
                    Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
 End StringToIdent.