From 9e0cc537deb622fe901e8e467995c7131e1a1035 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Aug 2024 22:21:16 +0200
Subject: [PATCH] Move Ltac2 `compute` back into `StringToIdent` module.
---
iris/proofmode/string_ident.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 27130890f..c4a6e9479 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 :=
--
GitLab