Renaming local_binder into local_binder_expr.

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

18 files changed, 62 insertions, 62 deletions

diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index a92da035f..9f200edef 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -23,8 +23,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
 (** Equality on [constr_expr]. This is a syntactical one, which is oblivious to
     some parsing details, including locations. *)
 
-val local_binder_eq : local_binder -> local_binder -> bool
-(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *)
+val local_binder_eq : local_binder_expr -> local_binder_expr -> bool
+(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *)
 
 val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
 (** Equality on [binding_kind] *)
@@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
 val constr_loc : constr_expr -> Loc.t
 val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
 val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
-val local_binders_loc : local_binder list -> Loc.t
+val local_binders_loc : local_binder_expr list -> Loc.t
 
 (** {6 Constructors}*)
 
@@ -49,19 +49,19 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
 val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr
 val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
-val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
 
-val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [abstract_constr_expr], with location *)
 
-val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
+val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [prod_constr_expr], with location *)
 
 val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
 val expand_pattern_binders :
-  (Loc.t -> local_binder list -> constr_expr -> constr_expr) ->
-  local_binder list -> constr_expr -> local_binder list * constr_expr
+  (Loc.t -> local_binder_expr list -> constr_expr -> constr_expr) ->
+  local_binder_expr list -> constr_expr -> local_binder_expr list * constr_expr
 
 (** {6 Destructors}*)
 
@@ -78,9 +78,9 @@ val coerce_to_name : constr_expr -> Name.t located
 
 val default_binder_kind : binder_kind
 
-val names_of_local_binders : local_binder list -> Name.t located list
+val names_of_local_binders : local_binder_expr list -> Name.t located list
 (** Retrieve a list of binding names from a list of binders. *)
 
-val names_of_local_assums : local_binder list -> Name.t located list
-(** Same as [names_of_local_binders], but does not take the [let] bindings into
+val names_of_local_assums : local_binder_expr list -> Name.t located list
+(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
     account. *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index f617faa38..b39339450 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -41,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> sorts -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
-  Context.Rel.t -> local_binder list
+  Context.Rel.t -> local_binder_expr list
 
 (** Printing options *)
 val print_implicits : bool ref
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d99747be5..e45de2588 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,7 +88,7 @@ val intern_gen : typing_constraint -> env ->
 val intern_pattern : env -> cases_pattern_expr ->
   Id.t list * (Id.t Id.Map.t * cases_pattern) list
 
-val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_decl list
+val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
 (** {6 Composing internalization with type inference (pretyping) } *)
 
@@ -157,16 +157,16 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types
 
 val interp_context_evars :
   ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
-  env -> evar_map ref -> local_binder list ->
+  env -> evar_map ref -> local_binder_expr list ->
   internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits)
 
 (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
 (*   (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
 (*   ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
+(*   env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
   
 (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
-(*   env -> evar_map -> local_binder list ->  *)
+(*   env -> evar_map -> local_binder_expr list ->  *)
 (*   internalization_env *  *)
 (*   ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index fe0e8d44b..4caacc08c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -102,7 +102,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
 let ids_of_names l =
   List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
 
-let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
+let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
   let rec aux bdvars l c = match c with
       ((LocalRawAssum (n, _, c)) :: tl) ->
 	let bound = ids_of_names n in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d0327e506..71009ec3c 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -25,7 +25,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
   Id.t list -> Id.t list
 
 val free_vars_of_binders :
-  ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list
+  ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list
 
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurrence *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 95d702f8d..b6ac40041 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -25,7 +25,7 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool
 (** Specific function for interning "in indtype" syntax of "match" *)
 val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
 
-val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list
+val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
 
 (** Used in typeclasses *)
 
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index f7aa72279..c2ace9dc2 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 8827bc132..a9f710639 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 *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 07e4ddf84..496b20002 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -233,11 +233,11 @@ type (_, _) entry =
 | TTName : ('self, Name.t Loc.located) entry
 | TTReference : ('self, reference) entry
 | TTBigint : ('self, Bigint.bigint) entry
-| TTBinder : ('self, local_binder list) entry
+| TTBinder : ('self, local_binder_expr list) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
 | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
-| TTBinderListT : ('self, local_binder list) entry
-| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry
+| TTBinderListT : ('self, local_binder_expr list) entry
+| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry
 
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
@@ -324,7 +324,7 @@ let cases_pattern_expr_of_name (loc,na) = match na with
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
-  binders : (local_binder list * bool) list;
+  binders : (local_binder_expr list * bool) list;
 }
 
 let push_constr subst v = { subst with constrs = v :: subst.constrs }
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cf5174af9..6c148d393 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -162,11 +162,11 @@ module Constr :
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
-    val closed_binder : local_binder list Gram.entry
-    val binder : local_binder list Gram.entry (* closed_binder or variable *)
-    val binders : local_binder list Gram.entry (* list of binder *)
-    val open_binders : local_binder list Gram.entry
-    val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry
+    val closed_binder : local_binder_expr list Gram.entry
+    val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
+    val binders : local_binder_expr list Gram.entry (* list of binder *)
+    val open_binders : local_binder_expr list Gram.entry
+    val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry
     val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry
     val record_declaration : constr_expr Gram.entry
     val appl_arg : (constr_expr * explicitation located option) Gram.entry
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8d5b1e782..de2fabb9e 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 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
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index a0106837a..f92caf426 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -19,12 +19,12 @@ open Names
 open Misctypes
 
 val extract_lam_binders :
-  constr_expr -> local_binder list * constr_expr
+  constr_expr -> local_binder_expr list * constr_expr
 val extract_prod_binders :
-  constr_expr -> local_binder list * constr_expr
+  constr_expr -> local_binder_expr list * constr_expr
 val split_fix :
   int -> constr_expr -> constr_expr ->
-  local_binder list *  constr_expr * constr_expr
+  local_binder_expr list *  constr_expr * constr_expr
 
 val prec_less : int -> int * Ppextend.parenRelation -> bool
 
@@ -50,12 +50,12 @@ val pr_patvar : patvar -> std_ppcmds
 val pr_glob_level : glob_level -> std_ppcmds
 val pr_glob_sort : glob_sort -> std_ppcmds
 val pr_guard_annot : (constr_expr -> std_ppcmds) ->
-  local_binder list ->
+  local_binder_expr list ->
   ('a * Names.Id.t) option * recursion_order_expr ->
   std_ppcmds
 
 val pr_record_body : (reference * constr_expr) list -> std_ppcmds
-val pr_binders : local_binder list -> std_ppcmds
+val pr_binders : local_binder_expr list -> std_ppcmds
 val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
 val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
 val pr_constr_expr : constr_expr -> std_ppcmds
diff --git a/vernac/classes.mli b/vernac/classes.mli
index d2cb788ea..69ea84158 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -42,7 +42,7 @@ val new_instance :
   ?global:bool -> (** Not global by default. *)
   ?refine:bool -> (** Allow refinement *)
   Decl_kinds.polymorphic ->
-  local_binder list ->
+  local_binder_expr list ->
   typeclass_constraint ->
   (bool * constr_expr) option ->
   ?generalize:bool ->
@@ -63,4 +63,4 @@ val id_of_class : typeclass -> Id.t
 
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
-val context : Decl_kinds.polymorphic -> local_binder list -> bool
+val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool
diff --git a/vernac/command.ml b/vernac/command.ml
index 264f5f336..edd2401c7 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -370,7 +370,7 @@ type structured_one_inductive_expr = {
 }
 
 type structured_inductive_expr =
-  local_binder list * structured_one_inductive_expr list
+  local_binder_expr list * structured_one_inductive_expr list
 
 let minductive_message warn = function
   | []  -> error "No inductive definition."
@@ -830,7 +830,7 @@ type structured_fixpoint_expr = {
   fix_name : Id.t;
   fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
-  fix_binders : local_binder list;
+  fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
   fix_type : constr_expr
 }
diff --git a/vernac/command.mli b/vernac/command.mli
index 616afb91f..bccc22ae9 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+  lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
@@ -41,13 +41,13 @@ val declare_definition : Id.t -> definition_kind ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
 val do_definition : Id.t -> definition_kind -> lident list option ->
-  local_binder list -> red_expr option -> constr_expr ->
+  local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
 (** {6 Parameters/Assumptions} *)
 
 (* val interp_assumption : env -> evar_map ref -> *)
-(*   local_binder list -> constr_expr ->  *)
+(*   local_binder_expr list -> constr_expr ->  *)
 (*   types Univ.in_universe_context_set * Impargs.manual_implicits *)
 
 (** returns [false] if the assumption is neither local to a section,
@@ -78,7 +78,7 @@ type structured_one_inductive_expr = {
 }
 
 type structured_inductive_expr =
-  local_binder list * structured_one_inductive_expr list
+  local_binder_expr list * structured_one_inductive_expr list
 
 val extract_mutual_inductive_declaration_components :
   (one_inductive_expr * decl_notation list) list ->
@@ -114,7 +114,7 @@ type structured_fixpoint_expr = {
   fix_name : Id.t;
   fix_univs : lident list option;
   fix_annot : Id.t Loc.located option;
-  fix_binders : local_binder list;
+  fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
   fix_type : constr_expr
 }
diff --git a/vernac/record.mli b/vernac/record.mli
index c50e57786..3fd651db9 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -39,7 +39,7 @@ val declare_structure :
 
 val definition_structure :
   inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
-  plident with_coercion * local_binder list *
+  plident with_coercion * local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference