diff options
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 0fd0548c29..917b3e02fb 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -58,6 +58,11 @@ val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic val general_s_rewrite_in : identifier -> bool -> constr -> new_goals:constr list -> tactic +val setoid_reflexivity : tactic +val setoid_symmetry : tactic +val setoid_symmetry_in : identifier -> tactic +val setoid_transitivity : constr -> tactic + val add_relation : Names.identifier -> constr_expr -> constr_expr -> constr_expr option -> constr_expr option -> constr_expr option -> unit |