From e1cf5ccd8df7080d7dd2aadf0305a9d3ba9c5d9d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 18 May 2014 13:03:54 -0400
Subject: Restored old behavior of injection on proofs by default.

Use Set Injection On Proof to enable the new behavior.
---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6e50b923b0..15a7746136 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -611,7 +611,7 @@ let replace_in_clause_maybe_by c2 c1 cl tac_opt =
 exception DiscrFound of
   (constructor * int) list * constructor * constructor
 
-let injection_on_proofs = ref true
+let injection_on_proofs = ref false
 
 let _ =
   declare_bool_option
-- 
cgit v1.2.3