From 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Dec 2016 19:45:04 +0100 Subject: 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. --- tactics/eqdecide.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'tactics/eqdecide.ml') diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d912decff..8764ef085 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) = clear_last; intros] +let inj_flags = Some { + Equality.keep_proof_equalities = true; (* necessary *) + Equality.injection_in_context = true; (* does not matter here *) + Equality.injection_pattern_l2r_order = true; (* does not matter here *) + } + let discrHyp id = let c env sigma = (sigma, (mkVar id, NoBindings)) in let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in @@ -136,7 +142,7 @@ let eqCase tac = let injHyp id = let c env sigma = (sigma, (mkVar id, NoBindings)) in - let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in + let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in Tacticals.New.tclDELAYEDWITHHOLES false c tac let diseqCase hyps eqonleft = -- cgit v1.2.3