From 0746578040e738d079bcc3289857bb99983a7a22 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 30 Sep 2016 11:52:21 +0200
Subject: fixing bug 4609: document an option governing the generation of
 equalities between proofs in tactic injection, with a side-effect on
 inversion.

---
 tactics/equality.ml | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'tactics')

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