diff options
| author | Maxime Dénès | 2017-10-27 18:01:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-27 18:01:42 +0200 |
| commit | bb383ae81838aabae9fe77fdbeaecf46bb85b4f2 (patch) | |
| tree | e2b9ab6963e145b558d9651e4fca922648546eb1 /plugins/funind/invfun.ml | |
| parent | ad973248998da8d7d10ed00f4bcd6f383ba9a171 (diff) | |
| parent | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (diff) | |
Merge PR #677: Trunk+abstracting injection flags
Diffstat (limited to 'plugins/funind/invfun.ml')
| -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 9cb2a0a3f5..93317fce1b 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 ) |