diff options
Diffstat (limited to 'tactics/rewrite.mli')
| -rw-r--r-- | tactics/rewrite.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 9bdfc08d2..0f155c8bb 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -41,6 +41,10 @@ val cl_rewrite_clause : interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> bool -> Locus.occurrences -> Id.t option -> tactic +val cl_rewrite_clause_newtac' : + interp_sign * (glob_constr_and_expr * glob_constr_and_expr bindings) -> + bool -> Locus.occurrences -> Id.t option -> unit Proofview.tactic + val is_applied_rewrite_relation : env -> evar_map -> Context.rel_context -> constr -> types option @@ -57,6 +61,12 @@ val add_morphism_infer : bool -> constr_expr -> Id.t -> unit val add_morphism : bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit +val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr + +val get_symmetric_proof : env -> evar_map -> constr -> constr -> evar_map * constr + +val get_transitive_proof : env -> evar_map -> constr -> constr -> evar_map * constr + val default_morphism : (types * constr option) option list * (types * types option) option -> constr -> constr * constr |