Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.

2 files changed, 13 insertions, 13 deletions

diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index f7aa722799..c2ace9dc27 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -111,10 +111,10 @@ and binder_expr =
 
 and fix_expr =
     Id.t located * (Id.t located option * recursion_order_expr) *
-      local_binder list * constr_expr * constr_expr
+      local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
-    Id.t located * local_binder list * constr_expr * constr_expr
+    Id.t located * local_binder_expr list * constr_expr * constr_expr
 
 and recursion_order_expr =
   | CStructRec
@@ -122,7 +122,7 @@ and recursion_order_expr =
   | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
 
 (** Anonymous defs allowed ?? *)
-and local_binder =
+and local_binder_expr =
   | LocalRawAssum of Name.t located list * binder_kind * constr_expr
   | LocalRawDef of Name.t located * constr_expr
   | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option
@@ -130,7 +130,7 @@ and local_binder =
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
     constr_expr list list * (** for recursive notations *)
-    local_binder list list (** for binders subexpressions *)
+    local_binder_expr list list (** for binders subexpressions *)
 
 type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr
 
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 8827bc132e..a9f7106395 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -175,15 +175,15 @@ type plident = lident * lident list option
 type sort_expr = glob_sort
 
 type definition_expr =
-  | ProveBody of local_binder list * constr_expr
-  | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr
+  | ProveBody of local_binder_expr list * constr_expr
+  | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr
       * constr_expr option
 
 type fixpoint_expr =
-    plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option
+    plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
-    plident * local_binder list * constr_expr * constr_expr option
+    plident * local_binder_expr list * constr_expr * constr_expr option
 
 type local_decl_expr =
   | AssumExpr of lname * constr_expr
@@ -202,14 +202,14 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
 type inductive_expr =
-  plident with_coercion * local_binder list * constr_expr option * inductive_kind *
+  plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  plident * local_binder list * constr_expr option * constructor_expr list
+  plident * local_binder_expr list * constr_expr option * constructor_expr list
 
 type proof_expr =
-  plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
+  plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option)
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
@@ -370,12 +370,12 @@ type vernac_expr =
   (* Type classes *)
   | VernacInstance of
       bool * (* abstract instance *)
-      local_binder list * (* super *)
+      local_binder_expr list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(bool * constr_expr) option * (* props *)
 	hint_info_expr
 
-  | VernacContext of local_binder list
+  | VernacContext of local_binder_expr list
 
   | VernacDeclareInstances of
     (reference * hint_info_expr) list (* instances names, priorities and patterns *)