diff options
| author | Hugo Herbelin | 2016-12-05 11:36:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-23 22:13:56 +0100 |
| commit | 8f5d447769a41cd251701272a6ff71a7a20de658 (patch) | |
| tree | 8146cf9cdfc399f43e2ecd9bd9df49dfae49b635 /interp/constrexpr_ops.mli | |
| parent | 80d36bc6538b7feaab3dfa43f6e234ae85b55692 (diff) | |
Improving the API of constrexpr_ops.mli.
Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.
Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.
So, there is also a "fix" of semantic here.
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f6..7d3011a6e1 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -49,14 +49,14 @@ 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 mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr -(** Same as [abstract_constr_expr], with location *) - val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr -(** Same as [prod_constr_expr], with location *) + +(** @deprecated variant of mkCLambdaN *) +val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr + +(** @deprecated variant of mkCProdN *) +val prod_constr_expr : constr_expr -> local_binder list -> constr_expr val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t val expand_pattern_binders : |