From f0311f2004e148d98c12ddc91fe01dc630b058c1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 13 Jul 2024 10:55:40 -0700 Subject: [PATCH] compatibility with coq/coq#19310 coq/coq#19310 rewrites the Coq prefix to Stdlib on the fly --- src/Util/ZUtil/Hints/Core.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Util/ZUtil/Hints/Core.v b/src/Util/ZUtil/Hints/Core.v index 08c443ace7..52858825fb 100644 --- a/src/Util/ZUtil/Hints/Core.v +++ b/src/Util/ZUtil/Hints/Core.v @@ -112,6 +112,15 @@ Module Coq. End PreOmega. End omega. End Coq. +Module Stdlib. + Module omega. + Module PreOmega. + Definition Z_of_nat' := Z.of_nat. + Ltac hide_Z_of_nat a := idtac. + Ltac zify_nat_op := idtac. + End PreOmega. + End omega. +End Stdlib. Ltac Coq.omega.PreOmega.zify_nat_op ::= match goal with