From 1948023891d26e628397a303263b912225f2cc31 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 21 Aug 2016 22:09:01 +0200
Subject: Documenting "Set Structural Injection".

---
 doc/refman/RefMan-tac.tex | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'doc')

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}
 
-- 
cgit v1.2.3


From 50bece7c25e62132bc06c3bb0261937c657319d3 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 22 Aug 2016 15:31:24 -0400
Subject: update Proof General URL

---
 doc/faq/fk.bib            | 2 +-
 doc/refman/RefMan-uti.tex | 2 +-
 doc/refman/biblio.bib     | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

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-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,
-- 
cgit v1.2.3