From 01d663f58854c1e504efae8ba583425cd998d211 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 19 Feb 2024 12:03:55 +0100
Subject: [PATCH] Code review in Compl is completed. Add some doc.

---
 FEM/Compl/Compl.v          | 11 ++++++++++-
 FEM/Compl/Function_compl.v |  2 +-
 FEM/Compl/Function_sub.v   |  4 +++-
 3 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/FEM/Compl/Compl.v b/FEM/Compl/Compl.v
index 30238f5c..9fac6b03 100644
--- a/FEM/Compl/Compl.v
+++ b/FEM/Compl/Compl.v
@@ -14,7 +14,16 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-(** Export of complements. *)
+(** Export complements for finite elements.
+
+  Uses classical logic, functional extensionality,
+       decidability on subsets (emptiness, belonging),
+       non-unique choice.
+
+  Provides 'propositional_extensionality' as 'prop_ext',
+           'proof_irrelevance' as 'proof_irrel',
+           'constructive_indefinite_description' as 'ex_EX'.
+ *)
 
 From FEM.Compl Require Export logic_compl.
 From FEM.Compl Require Export Subset_compl Function_compl Function_sub.
diff --git a/FEM/Compl/Function_compl.v b/FEM/Compl/Function_compl.v
index 536da869..acdb5493 100644
--- a/FEM/Compl/Function_compl.v
+++ b/FEM/Compl/Function_compl.v
@@ -18,7 +18,7 @@ COPYING file for more details.
 From Coq Require Import ClassicalChoice.
 From Coq Require Import ssreflect ssrfun.
 
-(* We need decidability of the belonging to a subset, and functional extensionality. *)
+(* We need decidability of the belonging to subsets, and functional extensionality. *)
 From Lebesgue Require Import Subset Subset_dec Function.
 
 (* We need classical logic, and a constructive form of indefinite description. *)
diff --git a/FEM/Compl/Function_sub.v b/FEM/Compl/Function_sub.v
index 2b2d9229..503397bc 100644
--- a/FEM/Compl/Function_sub.v
+++ b/FEM/Compl/Function_sub.v
@@ -14,12 +14,14 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 COPYING file for more details.
 *)
 
-(* We need "non-unique" choice. *)
+(* We need non-unique choice. *)
 From Coq Require Import ClassicalChoice.
 From Coq Require Import ssreflect ssrfun.
 
+(* We need decidability of the belonging to subsets. *)
 From Lebesgue Require Import Subset Subset_dec Function.
 
+(* We need classical logic, and a constructive form of indefinite description. *)
 From FEM Require Import logic_compl Function_compl.
 
 
-- 
GitLab