From 1ac0db9ac133b8030147cbbf4499a799a6244ec0 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 22 Oct 2021 12:25:10 +0900
Subject: [PATCH] add doc targets to makefile

- also remove a few spurious comments
---
 CHANGELOG_UNRELEASED.md |  3 +++
 Makefile.common         | 24 ++++++++++++++++++++++++
 theories/normedtype.v   |  6 +++---
 3 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bdc8..e6536bb26 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -12,4 +12,7 @@
 
 ### Infrastructure
 
+- in `Makefile.common`
+  + add `doc` and `doc-clean` targets
+
 ### Misc
diff --git a/Makefile.common b/Makefile.common
index c52341072..9acb5d9f5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -97,3 +97,27 @@ endif
 # Make of individual .vo ---------------------------------------------
 %.vo: __always__ Makefile.coq
 	+$(COQMAKE) $@
+
+# the doc targets are essentially copied from the Mathematical Components repository
+# the location of the math-comp git repository is hard-wired to avoid copying scripts
+MATHCOMP = ../math-comp/
+
+doc: __always__ Makefile.coq
+	mkdir -p _build_doc/
+	cp -r $(COQFILES) -t _build_doc/ --parents
+	cp _CoqProject Makefile* _build_doc
+	mkdir -p _build_doc/htmldoc
+	. $(MATHCOMP)etc/utils/builddoc_lib.sh; \
+		cd _build_doc && mangle_sources $(COQFILES)
+	+cd _build_doc && $(COQMAKE)
+# let's forget about the dependency graph for the time being...
+#	cd _build_doc && grep -v vio: .Makefile.coq.d > depend
+#	cd _build_doc && cat depend | $(MATHCOMP)etc/buildlibgraph $(COQFILES) > htmldoc/depend.js
+	cd _build_doc && $(COQBIN)coqdoc -t "MathComp Analysis" \
+		-g --utf8 -R theories mathcomp.analysis \
+		--parse-comments \
+		--multi-index $(COQFILES) -d htmldoc
+	cp $(MATHCOMP)etc/artwork/coqdoc.css _build_doc/htmldoc
+
+doc-clean:
+	rm -rf _build_doc/
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 22b08e2c3..474b0e4ef 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -299,7 +299,7 @@ Proof. by case: V => ? [? ? ? ? ? ? []]. Qed.
 
 End pseudoMetricnormedzmodule_lemmas.
 
-(** locally *)
+(** neighborhoods *)
 
 Section Nbhs'.
 Context {R : numDomainType} {T : pseudoMetricType R}.
@@ -392,7 +392,7 @@ Global Instance Proper_dnbhs_realType (R : realType) (x : R) :
   ProperFilter x^'.
 Proof. exact: Proper_dnbhs_numFieldType. Qed.
 
-(** * Some Topology on [Rbar] *)
+(** * Some Topology on extended real numbers *)
 
 Definition pinfty_nbhs (R : numFieldType) : set (set R) :=
   fun P => exists M, M \is Num.real /\ forall x, M < x -> P x.
@@ -3329,7 +3329,7 @@ Grab Existential Variables. all: end_near. Qed.
 
 (** Local properties in [R] *)
 
-(** * Topology on [R]² *)
+(* Topology on [R]² *)
 
 (* Lemma locally_2d_align : *)
 (*   forall (P Q : R -> R -> Prop) x y, *)