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. --- interp/constrexpr_ops.mli | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'interp/constrexpr_ops.mli') 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. *) -- cgit v1.2.3