diff options
| author | Gaëtan Gilbert | 2018-10-11 17:04:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | f041d16b65d05074e1fea90a654aa3e7f000b6dc (patch) | |
| tree | d6cac53d6755f8d3d438306de0bbde27198925ef /plugins/ltac/rewrite.mli | |
| parent | 0fa0ad02cb17a19edcd81efc8e41ccdd4f37ffaf (diff) | |
rewrite: attributes handle is_univ_poly, is_program_mode
Diffstat (limited to 'plugins/ltac/rewrite.mli')
| -rw-r--r-- | plugins/ltac/rewrite.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 0d014a0bf3..4f46e78c71 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -19,6 +19,9 @@ open Tacinterp (** TODO: document and clean me! *) +type rewrite_attributes +val rewrite_attributes : rewrite_attributes Attributes.attribute + type unary_strategy = Subterms | Subterm | Innermost | Outermost | Bottomup | Topdown | Progress | Try | Any | Repeat @@ -77,18 +80,18 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : ?locality:bool -> +val declare_relation : rewrite_attributes -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit val add_setoid : - bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> unit -val add_morphism_infer : bool -> constr_expr -> Id.t -> unit +val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism : - bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit + rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr |