diff options
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 116 |
1 files changed, 49 insertions, 67 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 75a59e6d..90d8a224 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,29 +1,21 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i*) -open Util open Names open Term -open Sign open Evd open Environ -open Proof_type open Tacmach -open Hipattern -open Pattern -open Tacticals -open Tactics open Tacexpr -open Termops -open Glob_term -open Genarg open Ind_tables +open Locus +open Misctypes (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) @@ -38,101 +30,91 @@ type conditions = val general_rewrite_bindings : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> - ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic + ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> evars_flag -> unit Proofview.tactic val general_rewrite : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> - ?tac:(tactic * conditions) -> constr -> tactic + ?tac:(unit Proofview.tactic * conditions) -> constr -> unit Proofview.tactic (* Equivalent to [general_rewrite l2r] *) -val rewriteLR : ?tac:(tactic * conditions) -> constr -> tactic -val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic +val rewriteLR : ?tac:(unit Proofview.tactic * conditions) -> constr -> unit Proofview.tactic +val rewriteRL : ?tac:(unit Proofview.tactic * conditions) -> constr -> unit Proofview.tactic (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *) -val register_general_rewrite_clause : - (identifier option -> orientation -> - occurrences -> constr with_bindings -> new_goals:constr list -> tactic) -> unit -val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit +val general_setoid_rewrite_clause : + (Id.t option -> orientation -> occurrences -> constr with_bindings -> + new_goals:constr list -> unit Proofview.tactic) Hook.t -val general_rewrite_ebindings_clause : identifier option -> +val general_rewrite_ebindings_clause : Id.t option -> orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> - ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic + ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> evars_flag -> unit Proofview.tactic val general_rewrite_bindings_in : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> - ?tac:(tactic * conditions) -> - identifier -> constr with_bindings -> evars_flag -> tactic + ?tac:(unit Proofview.tactic * conditions) -> + Id.t -> constr with_bindings -> evars_flag -> unit Proofview.tactic val general_rewrite_in : orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> - ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic + ?tac:(unit Proofview.tactic * conditions) -> Id.t -> constr -> evars_flag -> unit Proofview.tactic + +val general_rewrite_clause : + orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic val general_multi_rewrite : - orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic - -type delayed_open_constr_with_bindings = - env -> evar_map -> evar_map * constr with_bindings - -val general_multi_multi_rewrite : - evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> - clause -> (tactic * conditions) option -> tactic - -val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic -val replace : constr -> constr -> tactic -val replace_in : identifier -> constr -> constr -> tactic -val replace_by : constr -> constr -> tactic -> tactic -val replace_in_by : identifier -> constr -> constr -> tactic -> tactic - -val discr : evars_flag -> constr with_bindings -> tactic -val discrConcl : tactic -val discrClause : evars_flag -> clause -> tactic -val discrHyp : identifier -> tactic -val discrEverywhere : evars_flag -> tactic + evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list -> + clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic + +val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.tactic option -> unit Proofview.tactic +val replace : constr -> constr -> unit Proofview.tactic +val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic + +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 induction_arg option -> tactic -val inj : intro_pattern_expr located list -> evars_flag -> - constr with_bindings -> tactic -val injClause : intro_pattern_expr located list -> evars_flag -> - constr with_bindings induction_arg option -> tactic -val injHyp : identifier -> tactic -val injConcl : tactic + constr with_bindings induction_arg option -> unit Proofview.tactic +val inj : intro_patterns option -> evars_flag -> + clear_flag -> constr with_bindings -> unit Proofview.tactic +val injClause : intro_patterns option -> evars_flag -> + constr with_bindings induction_arg option -> unit Proofview.tactic +val injHyp : clear_flag -> Id.t -> unit Proofview.tactic +val injConcl : unit Proofview.tactic -val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic -val dEqThen : evars_flag -> (int -> tactic) -> constr with_bindings induction_arg option -> tactic +val dEq : evars_flag -> constr with_bindings induction_arg option -> unit Proofview.tactic +val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings induction_arg option -> unit Proofview.tactic val make_iterated_tuple : - env -> evar_map -> constr -> (constr * types) -> constr * constr * constr + env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) (* The family cutRewriteIn expect an equality statement *) -val cutRewriteInHyp : bool -> types -> identifier -> tactic -val cutRewriteInConcl : bool -> constr -> tactic +val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic +val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic (* The family rewriteIn expect the proof of an equality *) -val rewriteInHyp : bool -> constr -> identifier -> tactic -val rewriteInConcl : bool -> constr -> tactic - -(* Expect the proof of an equality; fails with raw internal errors *) -val substClause : bool -> constr -> identifier option -> tactic +val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic +val rewriteInConcl : bool -> constr -> unit Proofview.tactic val discriminable : env -> evar_map -> constr -> constr -> bool val injectable : env -> evar_map -> constr -> constr -> bool (* Subst *) -val unfold_body : identifier -> tactic +(* val unfold_body : Id.t -> tactic *) type subst_tactic_flags = { only_leibniz : bool; rewrite_dependent_proof : bool } -val subst_gen : bool -> identifier list -> tactic -val subst : identifier list -> tactic -val subst_all : ?flags:subst_tactic_flags -> tactic +val subst_gen : bool -> Id.t list -> unit Proofview.tactic +val subst : Id.t list -> unit Proofview.tactic +val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic (* Replace term *) -(* [replace_multi_term dir_opt c cl] +(* [replace_term dir_opt c cl] perfoms replacement of [c] by the first value found in context (according to [dir] if given to get the rewrite direction) in the clause [cl] *) -val replace_multi_term : bool option -> constr -> clause -> tactic +val replace_term : bool option -> constr -> clause -> unit Proofview.tactic val set_eq_dec_scheme_kind : mutual scheme_kind -> unit |