From 89f09d26cee2588b1e3dea005dd28a0e52224198 Mon Sep 17 00:00:00 2001 From: Amlal El Mahrouss Date: Thu, 29 Jan 2026 12:41:37 +0100 Subject: chore: Fix warning on newer versions of Rocq. Signed-off-by: Amlal El Mahrouss --- proofs/WG05/ExecutionAuthority.v | 2 +- proofs/WG05/ExecutionDomains.v | 4 ++-- proofs/WG05/HarvardSeparation.v | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'proofs') diff --git a/proofs/WG05/ExecutionAuthority.v b/proofs/WG05/ExecutionAuthority.v index 85a5872..c4e2ca3 100644 --- a/proofs/WG05/ExecutionAuthority.v +++ b/proofs/WG05/ExecutionAuthority.v @@ -8,7 +8,7 @@ Formalization: January 2026 *) -Require Import Logic.Classical_Prop. +From Stdlib Require Import Logic.Classical_Prop. Require Import WG05.ExecutionDomains. (** * Traits *) diff --git a/proofs/WG05/ExecutionDomains.v b/proofs/WG05/ExecutionDomains.v index 519bb23..27186f1 100644 --- a/proofs/WG05/ExecutionDomains.v +++ b/proofs/WG05/ExecutionDomains.v @@ -8,8 +8,8 @@ Formalization: January 2026 *) -Require Import Logic.Classical_Prop. -Require Import Logic.FunctionalExtensionality. +From Stdlib Require Import Logic.Classical_Prop. +From Stdlib Require Import Logic.FunctionalExtensionality. (** * Execution Contexts *) diff --git a/proofs/WG05/HarvardSeparation.v b/proofs/WG05/HarvardSeparation.v index c067724..d6d4872 100644 --- a/proofs/WG05/HarvardSeparation.v +++ b/proofs/WG05/HarvardSeparation.v @@ -12,7 +12,7 @@ Formalization: January 2026 *) -Require Import Logic.Classical_Prop. +From Stdlib Require Import Logic.Classical_Prop. (** * Theory Structure *) -- cgit v1.2.3