diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-12-22 19:45:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-26 15:34:50 +0200 |
| commit | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (patch) | |
| tree | 770c08abffe9c2ea689cfa0f2e49cf9da445888c /plugins/funind | |
| parent | 925c434592597a34cd7ef4efb5e18a43e197bd96 (diff) | |
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.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/invfun.ml | 9 |
1 files changed, 7 insertions, 2 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 ) |