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 a92da035f6..9f200edeff 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 From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- interp/constrexpr_ops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrexpr_ops.mli') diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9f200edeff..45e3a19bc8 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -46,7 +46,7 @@ val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr +val mkLetInC : Name.t located * constr_expr * constr_expr option * 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_expr list -> constr_expr -- cgit v1.2.3