Passing around the flag for injection so that tactics calling inj at

ML level can set the flags themselves.

In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".

This fixes bug #5281.

3 files changed, 23 insertions, 18 deletions

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9cb2a0a3f..93317fce1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -570,6 +570,11 @@ let rec reflexivity_with_destruct_cases g =
     with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
   let eq_ind = make_eq () in
+  let my_inj_flags = Some {
+    Equality.keep_proof_equalities = false;
+    injection_in_context = false; (* for compatibility, necessary *)
+    injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *)
+  } in
   let discr_inject =
     Tacticals.onAllHypsAndConcl (
        fun sc g ->
@@ -580,8 +585,8 @@ let rec reflexivity_with_destruct_cases g =
 		 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
+		     else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2
+		     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a7aebf9e1..65c186a41 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -91,12 +91,12 @@ let elimOnConstrWithHoles tac with_evars c =
     (fun c -> tac with_evars (Some (None,ElimOnConstr c)))
 
 TACTIC EXTEND simplify_eq
-  [ "simplify_eq" ] -> [ dEq false None ]
-| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq false c ]
+  [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ]
+| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ]
 END
 TACTIC EXTEND esimplify_eq
-| [ "esimplify_eq" ] -> [ dEq true None ]
-| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles dEq true c ]
+| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ]
+| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ]
 END
 
 let discr_main c = elimOnConstrWithHoles discr_tac false c
@@ -117,31 +117,31 @@ let discrHyp id =
   discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings)))
 
 let injection_main with_evars c =
- elimOnConstrWithHoles (injClause None) with_evars c
+ elimOnConstrWithHoles (injClause None None) with_evars c
 
 TACTIC EXTEND injection
-| [ "injection" ] -> [ injClause None false None ]
-| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) false c ]
+| [ "injection" ] -> [ injClause None None false None ]
+| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ]
 END
 TACTIC EXTEND einjection
-| [ "einjection" ] -> [ injClause None true None ]
-| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None) true c ]
+| [ "einjection" ] -> [ injClause None None true None ]
+| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ]
 END
 TACTIC EXTEND injection_as
 | [ "injection" "as" intropattern_list(ipat)] ->
-    [ injClause (Some ipat) false None ]
+    [ injClause None (Some ipat) false None ]
 | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    [ mytclWithHoles (injClause (Some ipat)) false c ]
+    [ mytclWithHoles (injClause None (Some ipat)) false c ]
 END
 TACTIC EXTEND einjection_as
 | [ "einjection" "as" intropattern_list(ipat)] ->
-    [ injClause (Some ipat) true None ]
+    [ injClause None (Some ipat) true None ]
 | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    [ mytclWithHoles (injClause (Some ipat)) true c ]
+    [ mytclWithHoles (injClause None (Some ipat)) true c ]
 END
 TACTIC EXTEND simple_injection
-| [ "simple" "injection" ] -> [ simpleInjClause false None ]
-| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
+| [ "simple" "injection" ] -> [ simpleInjClause None false None ]
+| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ]
 END
 
 let injHyp id =
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 832044909..26b5c5767 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -396,7 +396,7 @@ let revtoptac n0 gl =
 
 let equality_inj l b id c gl =
   let msg = ref "" in
-  try Proofview.V82.of_tactic (Equality.inj l b None c) gl
+  try Proofview.V82.of_tactic (Equality.inj None l b None c) gl
   with
     | Ploc.Exc(_,CErrors.UserError (_,s))
     | CErrors.UserError (_,s)