From ac1fc7949ae795bd4c80f3140489aa57efbed74e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 26 Nov 2024 14:28:04 +0100 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 --- src/coqutil/Tactics/reference_to_string.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/coqutil/Tactics/reference_to_string.v b/src/coqutil/Tactics/reference_to_string.v index 8cf12bb2..82dacadc 100644 --- a/src/coqutil/Tactics/reference_to_string.v +++ b/src/coqutil/Tactics/reference_to_string.v @@ -15,12 +15,12 @@ Ltac2 reference_of_constr c := Ltac2 constr_string_basename_of_reference r := constr_string_of_string (Ident.to_string (List.last (Env.path r))). Ltac2 constr_string_qualname_of_reference r := - match Ident.of_string "Stdlib" with + match Ident.of_string "Corelib" with | None => constr_string_of_string "" - | Some ident_Stdlib => - constr_string_of_string (String.join "." (List.map (fun x => if Ident.equal x ident_Stdlib then "Coq" else Ident.to_string x) (Env.path r))) + | Some ident_Corelib => + constr_string_of_string (String.join "." (List.map (fun x => if Ident.equal x ident_Corelib then "Coq" else Ident.to_string x) (Env.path r))) end. - (* replace above hack by definition below when requiring Coq >= 8.21 *) + (* replace above hack by definition below when requiring Rocq >= 9.0 *) (* constr_string_of_string (String.join "." (List.map Ident.to_string (Env.path r))). *) Ltac2 constr_string_basename_of_constr_reference c := constr_string_basename_of_reference (reference_of_constr c).