diff options
| author | Pierre-Marie Pédrot | 2016-11-18 20:35:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:53 +0100 |
| commit | 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 (patch) | |
| tree | f1ef11f826c498a78c9af6ffd9020fbc454dcd5e /tactics/equality.mli | |
| parent | 8b660087beb2209e52bc4412dc82c6727963c6a5 (diff) | |
Equality API using EConstr.
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 97f51ae202..5467b4af25 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -10,6 +10,7 @@ open Names open Term open Evd +open EConstr open Environ open Ind_tables open Locus @@ -60,30 +61,30 @@ val general_rewrite_clause : orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic val general_multi_rewrite : - evars_flag -> (bool * multi * clear_flag * EConstr.constr with_bindings delayed_open) list -> + 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 -> EConstr.constr with_bindings -> 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 -> - EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings destruction_arg option -> unit Proofview.tactic val inj : intro_patterns option -> evars_flag -> - clear_flag -> EConstr.constr with_bindings -> unit Proofview.tactic + clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : intro_patterns option -> evars_flag -> - EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic + 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 -> - EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEq : evars_flag -> EConstr.constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> EConstr.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 make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) @@ -96,8 +97,8 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic -val discriminable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool -val injectable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool +val discriminable : env -> evar_map -> constr -> constr -> bool +val injectable : env -> evar_map -> constr -> constr -> bool (* Subst *) |