From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:21:51 +0100
Subject: Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.
---
 plugins/funind/indfun.ml   | 2 +-
 plugins/ltac/g_rewrite.ml4 | 2 +-
 plugins/ltac/rewrite.mli   | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8d5b1e7828..de2fabb9e3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -813,7 +813,7 @@ let rec chop_n_arrow n t =
       | _ -> anomaly (Pp.str "Not enough products")
 
 
-let rec get_args b t : Constrexpr.local_binder list *
+let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
   match b with
     | Constrexpr.CLambdaN (loc, (nal_ta), b') ->
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b1c4f58eb8..c50100bf55 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 35c4483513..4fdce0c84f 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
 
-- 
cgit v1.2.3