diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v index 27130890f36e36a1e54431fc726136abcddbc24e..c4a6e9479f9a8a41d6fd8bd3bd2b4f8e55fcd78b 100644 --- a/iris/proofmode/string_ident.v +++ b/iris/proofmode/string_ident.v @@ -6,9 +6,6 @@ From iris.prelude Require Import options. Import List.ListNotations. Local Open Scope list. -Ltac2 compute (c : Init.constr) : Init.constr := - Std.eval_vm Init.None c. - Module StringToIdent. Import Ltac2. @@ -45,6 +42,9 @@ Module StringToIdent. | _ => Control.throw (NotStringLiteral s) end. + Ltac2 compute (c : constr) : constr := + Std.eval_vm None c. + (** [coq_string_to_string] converts a Gallina string in a constr to an Ltac2 native string *) Ltac2 coq_string_to_string (s : constr) : string :=