diff options
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 41 |
1 files changed, 27 insertions, 14 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 47cb6b82..c0be917a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,20 +1,22 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) open Names -open Term open Evd +open EConstr open Environ -open Tacexpr open Ind_tables open Locus open Misctypes +open Tactypes (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) @@ -67,23 +69,31 @@ val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.ta val replace : constr -> constr -> unit Proofview.tactic val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic +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 discr : evars_flag -> constr with_bindings -> unit Proofview.tactic val discrConcl : unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val inj : intro_patterns option -> evars_flag -> + +(* Below, if flag is [None], it takes the value from the dynamic value of the option *) +val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic -val injClause : intro_patterns option -> evars_flag -> +val injClause : inj_flags option -> intro_patterns option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val injHyp : clear_flag -> Id.t -> unit Proofview.tactic -val injConcl : unit Proofview.tactic -val simpleInjClause : evars_flag -> +val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic +val injConcl : inj_flags option -> unit Proofview.tactic +val simpleInjClause : inj_flags option -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) @@ -96,8 +106,11 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic +(* Tells if tactic "discriminate" is applicable *) val discriminable : env -> evar_map -> constr -> constr -> bool -val injectable : env -> evar_map -> constr -> constr -> bool + +(* Tells if tactic "injection" is applicable *) +val injectable : env -> evar_map -> keep_proofs:(bool option) -> constr -> constr -> bool (* Subst *) |