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 /API | |
| 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 'API')
| -rw-r--r-- | API/API.mli | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/API/API.mli b/API/API.mli index a41009fa2..5e41464c8 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5337,6 +5337,11 @@ sig | Naive | FirstSolved | AllMatches + type inj_flags = { + keep_proof_equalities : bool; (* One may want it or not *) + injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *) + injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *) + } val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> @@ -5345,20 +5350,20 @@ sig val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic - val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag -> + val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val general_multi_rewrite : Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list -> Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic - val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic + val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic val discr_tac : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic - val injClause : Tactypes.intro_patterns option -> Misctypes.evars_flag -> + val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic - val simpleInjClause : Misctypes.evars_flag -> + val simpleInjClause : inj_flags option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic @@ -5392,8 +5397,8 @@ sig ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool val discrHyp : Names.Id.t -> unit Proofview.tactic - val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool - val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic + val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool + val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic end |