diff options
| author | Amlal El Mahrouss <amlal@nekernel.org> | 2026-02-04 11:42:04 +0100 |
|---|---|---|
| committer | Amlal El Mahrouss <amlal@nekernel.org> | 2026-02-04 11:42:16 +0100 |
| commit | eee3b0421235f4e20cd132fbfd1663f3de66146c (patch) | |
| tree | dd28c1cef66e7a03946894bf46ef7b8fbb4f68b8 | |
| parent | 1e387868486474db11cf110d6105e8aa9d9882a3 (diff) | |
chore: modernize Coq imports.
Signed-off-by: Amlal El Mahrouss <amlal@nekernel.org>
| -rw-r--r-- | proofs/WG05/ExecutionAuthority.v | 4 | ||||
| -rw-r--r-- | proofs/WG05/ExecutionDomains.v | 4 | ||||
| -rw-r--r-- | proofs/WG05/HarvardSeparation.v | 2 |
3 files changed, 6 insertions, 4 deletions
diff --git a/proofs/WG05/ExecutionAuthority.v b/proofs/WG05/ExecutionAuthority.v index c4e2ca3..4dd83e9 100644 --- a/proofs/WG05/ExecutionAuthority.v +++ b/proofs/WG05/ExecutionAuthority.v @@ -8,7 +8,7 @@ Formalization: January 2026 *) -From Stdlib Require Import Logic.Classical_Prop. +From Coq Require Import Logic.Classical_Prop. Require Import WG05.ExecutionDomains. (** * Traits *) @@ -166,4 +166,6 @@ Proof. - apply H12. apply H23. exact H. Qed. +Print authorities_agree_trans. + End AdditionalProperties. diff --git a/proofs/WG05/ExecutionDomains.v b/proofs/WG05/ExecutionDomains.v index 27186f1..ff8e017 100644 --- a/proofs/WG05/ExecutionDomains.v +++ b/proofs/WG05/ExecutionDomains.v @@ -8,8 +8,8 @@ Formalization: January 2026 *) -From Stdlib Require Import Logic.Classical_Prop. -From Stdlib Require Import Logic.FunctionalExtensionality. +From Coq Require Import Logic.Classical_Prop. +From Coq Require Import Logic.FunctionalExtensionality. (** * Execution Contexts *) diff --git a/proofs/WG05/HarvardSeparation.v b/proofs/WG05/HarvardSeparation.v index d6d4872..68975f3 100644 --- a/proofs/WG05/HarvardSeparation.v +++ b/proofs/WG05/HarvardSeparation.v @@ -12,7 +12,7 @@ Formalization: January 2026 *) -From Stdlib Require Import Logic.Classical_Prop. +From Coq Require Import Logic.Classical_Prop. (** * Theory Structure *) |