From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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.
---
 vernac/classes.mli |  4 ++--
 vernac/command.ml  |  4 ++--
 vernac/command.mli | 10 +++++-----
 vernac/record.mli  |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'vernac')

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
 
-- 
cgit v1.2.3