Merge remote-tracking branch 'github/pr/304' into v8.6

Was PR#304: fixing bug 4609

3 files changed, 38 insertions, 6 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d23a49bc67..2da12c8d69 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2289,6 +2289,12 @@ 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.
 
+By default, \texttt{injection} only creates new equalities between
+terms whose type is in sort \texttt{Type} or \texttt{Set}, thus
+implementing a special behavior for objects that are proofs
+of a statement in \texttt{Prop}.  This behavior can be turned off
+by setting the option \texttt{Set Keep Proof Equalities}.
+\optindex{Keep Proof Equalities}
 \subsection{\tt inversion \ident}
 \tacindex{inversion}
 
@@ -2308,6 +2314,14 @@ latter is first introduced in the local context using
 stock the lemmas whenever the same instance needs to be inverted
 several times. See Section~\ref{Derive-Inversion}.
 
+\Rem Part of the behavior of the \texttt{inversion} tactic is to generate
+equalities between expressions that appeared in the hypothesis that is
+being processed.  By default, no equalities are generated if they relate
+two proofs (i.e. equalities between terms whose type is in
+sort \texttt{Prop}).  This behavior can be turned off by using the option
+\texttt{Set Keep Proof Equalities.}
+\optindex{Keep Proof Equalities}
+
 \begin{Variants}
 \item \texttt{inversion \num}
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 201a1e00e8..e9d08d7375 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -701,16 +701,16 @@ let replace_in_clause_maybe_by c1 c2 cl tac_opt =
 exception DiscrFound of
   (constructor * int) list * constructor * constructor
 
-let injection_on_proofs = ref false
+let keep_proof_equalities_for_injection = ref false
 
 let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
       optname  = "injection on prop arguments";
-      optkey   = ["Injection";"On";"Proofs"];
-      optread  = (fun () -> !injection_on_proofs) ;
-      optwrite = (fun b -> injection_on_proofs := b) }
+      optkey   = ["Keep";"Proof";"Equalities"];
+      optread  = (fun () -> !keep_proof_equalities_for_injection) ;
+      optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
 
 let find_positions env sigma t1 t2 =
@@ -755,7 +755,7 @@ let find_positions env sigma t1 t2 =
 	    project env sorts posn t1_0 t2_0
   in
   try
-    let sorts = if !injection_on_proofs then [InSet;InType;InProp]
+    let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
 		else [InSet;InType]
     in
     Inr (findrec sorts [] t1 t2)
@@ -1389,7 +1389,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   | Inl _ ->
      tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
   | Inr [] ->
-     let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
+     let suggestion =
+         if !keep_proof_equalities_for_injection then
+            "" else
+            " You can try to use option Set Keep Proof Equalities." in
      tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
   | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
      tclZEROMSG (str"Nothing to inject.")
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 8745cf2fbd..da2183841d 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -135,6 +135,21 @@ intros * [= H].
 exact H.
 Abort.
 
+(* Test the Keep Proof Equalities option. *)
+Set Keep Proof Equalities.
+Unset Structural Injection.
+
+Inductive pbool : Prop := Pbool1 | Pbool2.
+
+Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell.
+
+Goal Pbsc Pbool1 = Pbsc Pbool2 -> True.
+injection 1.
+match goal with
+ |- Pbool1 = Pbool2 -> True => idtac | |- True => fail
+end.
+Abort.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.