From 017ea1410452a7b3ce7c5777eaac63f527ac3cc4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 4 Apr 2026 20:14:11 +0200 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/1456 --- theories/Crypt/Casts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Crypt/Casts.v b/theories/Crypt/Casts.v index 62df6aaf..eacc6a50 100644 --- a/theories/Crypt/Casts.v +++ b/theories/Crypt/Casts.v @@ -1,5 +1,5 @@ Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format". -From mathcomp Require Import ssreflect ssrbool ssrnat choice fintype eqtype all_algebra. +From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat choice fintype eqtype all_algebra. Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format". Set Warnings "-notation-overridden,-hiding-delimiting-key".