Merge remote-tracking branch 'v8.6' into trunk

4 files changed, 12 insertions, 3 deletions

diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib
index 4d90efcdb1..3410427dee 100644
--- a/doc/faq/fk.bib
+++ b/doc/faq/fk.bib
@@ -2171,7 +2171,7 @@ Decomposition}},
 @Misc{ProofGeneral,
   author =	 {David Aspinall},
   title =	 {Proof General},
-  note =	 {\url{http://proofgeneral.inf.ed.ac.uk/}}
+  note =	 {\url{https://proofgeneral.github.io/}}
 }
 
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 21b72b8eff..b668239a6a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2280,6 +2280,15 @@ hypothesis.
 
 \end{Variants}
 
+\optindex{Structural Injection}
+
+It is possible to ensure that \texttt{injection {\term}} erases the
+original hypothesis and leaves the generated equalities in the context
+rather than putting them as antecedents of the current goal, as if
+giving \texttt{injection {\term} as} (with an empty list of names). To
+obtain this behavior, the option {\tt Set Structural Injection} must
+be activated. This option is off by default.
+
 \subsection{\tt inversion \ident}
 \tacindex{inversion}
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index c282083b5c..10271ce0ca 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
 files.
 
 {\ProofGeneral} is developed and distributed independently of the
-system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
+system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!.
 
 
 \section[Module specification]{Module specification\label{gallina}\ttindex{gallina}}
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 70ee1f41f0..e69725838e 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -1199,7 +1199,7 @@ Decomposition}},
 @Misc{ProofGeneral,
   author      = {David Aspinall},
   title       = {Proof General},
-  note        = {\url{http://proofgeneral.inf.ed.ac.uk/}}
+  note        = {\url{https://proofgeneral.github.io/}}
 }
 
 @Book{CoqArt,