diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 18 | ||||
| -rw-r--r-- | interp/constrexpr_ops.mli | 12 |
2 files changed, 9 insertions, 21 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 59c24900d2..7433336f8f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -363,21 +363,9 @@ let mkCLambdaN loc bll c = let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c -let rec abstract_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> - List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl - (abstract_constr_expr c bl) - | LocalPattern _::_ -> assert false - -let rec prod_constr_expr c = function - | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> - List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl - (prod_constr_expr c bl) - | LocalPattern _::_ -> assert false +(* Deprecated *) +let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c +let prod_constr_expr c bl = mkCProdN (local_binders_loc bl) bl c let coerce_reference_to_id = function | Ident (_,id) -> id 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 : |