diff options
Diffstat (limited to 'tactics/setoid_replace.mli')
| -rw-r--r-- | tactics/setoid_replace.mli | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index adc02fe94b..1fa80953c2 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -13,6 +13,25 @@ open Proof_type open Topconstr open Names +type relation = + { rel_a: constr ; + rel_aeq: constr; + rel_refl: constr option; + rel_sym: constr option; + rel_trans : constr option; + rel_quantifiers_no: int (* it helps unification *) + } + +type 'a relation_class = + Relation of 'a (* the rel_aeq of the relation or the relation*) + | Leibniz of constr option (* the carrier (if eq is partially instantiated)*) + +type 'a morphism = + { args : (bool option * 'a relation_class) list; + output : 'a relation_class; + lem : constr; + } + type morphism_signature = (bool option * constr_expr) list * constr_expr val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds @@ -23,6 +42,11 @@ val register_general_rewrite : (bool -> constr -> tactic) -> unit val print_setoids : unit -> unit val equiv_list : unit -> constr list +val default_relation_for_carrier : + ?filter:(relation -> bool) -> types -> relation relation_class +(* [default_morphism] raises Not_found *) +val default_morphism : + ?filter:(constr morphism -> bool) -> constr -> relation morphism val setoid_replace : constr option -> constr -> constr -> new_goals:constr list -> tactic |