diff options
| author | Amlal El Mahrouss <amlal@nekernel.org> | 2026-01-24 12:36:29 +0100 |
|---|---|---|
| committer | Amlal El Mahrouss <amlal@nekernel.org> | 2026-01-24 12:36:29 +0100 |
| commit | fddd171cdf5411a180450125aad2af58a1c291d6 (patch) | |
| tree | ee3f179b2a36344fd3c410d6cea26ec136a2ac4b /proofs | |
| parent | ba8e38ae21c60450169c09531352b3426dae153c (diff) | |
fix: WG05: Don't specify `Stdlib` namespace--as it may fail on other platforms.
Signed-off-by: Amlal El Mahrouss <amlal@nekernel.org>
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/WG05/ExecutionAuthority.v | 2 | ||||
| -rw-r--r-- | proofs/WG05/ExecutionDomains.v | 4 | ||||
| -rw-r--r-- | proofs/WG05/HarvardSeparation.v | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/proofs/WG05/ExecutionAuthority.v b/proofs/WG05/ExecutionAuthority.v index f4cb5e2..85a5872 100644 --- a/proofs/WG05/ExecutionAuthority.v +++ b/proofs/WG05/ExecutionAuthority.v @@ -8,7 +8,7 @@ Formalization: January 2026 *) -Require Import Stdlib.Logic.Classical_Prop. +Require Import Logic.Classical_Prop. Require Import WG05.ExecutionDomains. (** * Traits *) diff --git a/proofs/WG05/ExecutionDomains.v b/proofs/WG05/ExecutionDomains.v index 534840a..519bb23 100644 --- a/proofs/WG05/ExecutionDomains.v +++ b/proofs/WG05/ExecutionDomains.v @@ -8,8 +8,8 @@ Formalization: January 2026 *) -Require Import Stdlib.Logic.Classical_Prop. -Require Import Stdlib.Logic.FunctionalExtensionality. +Require Import Logic.Classical_Prop. +Require Import Logic.FunctionalExtensionality. (** * Execution Contexts *) diff --git a/proofs/WG05/HarvardSeparation.v b/proofs/WG05/HarvardSeparation.v index 127b57d..c067724 100644 --- a/proofs/WG05/HarvardSeparation.v +++ b/proofs/WG05/HarvardSeparation.v @@ -12,7 +12,7 @@ Formalization: January 2026 *) -Require Import Stdlib.Logic.Classical_Prop. +Require Import Logic.Classical_Prop. (** * Theory Structure *) |