add doc targets to makefile

- also remove a few spurious comments

CHANGELOG_UNRELEASED.md

@@ -12,4 +12,7 @@
 
 ### Infrastructure
 
+- in `Makefile.common`
+  + add `doc` and `doc-clean` targets
+
 ### Misc

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/

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, *)