diff options
| author | Maxime Dénès | 2017-11-24 12:46:57 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-24 12:46:57 +0100 |
| commit | 31794a1828a15acb95c235fd3166c511635add41 (patch) | |
| tree | fb09a6b201001ababc3030dc80fa9d729526c0a7 /plugins/ltac/rewrite.mli | |
| parent | 92c15a9b660b874ce3fa125b1f9bdf2e85c40f47 (diff) | |
| parent | 57f62f06419972ba799e451d2f56552dc1b2fb63 (diff) | |
Merge PR #6197: [plugin] Remove LocalityFixme über hack.
Diffstat (limited to 'plugins/ltac/rewrite.mli')
| -rw-r--r-- | plugins/ltac/rewrite.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 1306c590ba..17e7244b39 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -75,7 +75,7 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : +val declare_relation : ?locality:bool -> ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit |