# --- T2-COPYRIGHT-BEGIN ---
# t2/package/*/compcert/ztac-import.patch
# Copyright (C) 2025 The T2 SDE Project
# SPDX-License-Identifier: GPL-2.0 or patched project license
# --- T2-COPYRIGHT-END ---

--- CompCert-3.15/flocq/Core/Digits.v.vanilla	2024-12-13 11:06:04.000000000 +0100
+++ CompCert-3.15/flocq/Core/Digits.v	2025-07-21 18:00:53.689709111 +0200
@@ -21,6 +21,7 @@
 From Coq Require SpecFloat.
 
 Require Import Zaux.
+From Stdlib.micromega Require Ztac.
 
 Notation digits2_pos := SpecFloat.digits2_pos (only parsing).
 Notation Zdigits2 := SpecFloat.Zdigits2 (only parsing).