diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-02-02 18:21:51 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-24 12:17:35 +0100 |
| commit | 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b (patch) | |
| tree | 42dfb8c1b0d8db6b3c70da6d093de9b4fec2385c /plugins/ltac | |
| parent | 68ffb813a0e1c7d62dac4769d0104210c2e5f6e9 (diff) | |
Renaming local_binder into local_binder_expr.
This is a bit long, but it is to keep a symmetry with constr_expr.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b1c4f58eb..c50100bf5 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF [ declare_relation a aeq n None None (Some lemma3) ] END -type binders_argtype = local_binder list +type binders_argtype = local_binder_expr list let wit_binders = (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 35c448351..4fdce0c84 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -77,17 +77,17 @@ val is_applied_rewrite_relation : env -> evar_map -> Context.Rel.t -> constr -> types option val declare_relation : - ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> + ?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 list -> constr_expr -> constr_expr -> constr_expr -> + bool -> 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 : - bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit + bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr |