diff options
Diffstat (limited to 'interp/constrexpr_ops.mli')
-rw-r--r-- | interp/constrexpr_ops.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index b547288e3..0ff51b060 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -34,9 +34,9 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool (** {6 Retrieving locations} *) -val constr_loc : constr_expr -> Loc.t -val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t -val local_binders_loc : local_binder_expr list -> Loc.t +val constr_loc : constr_expr -> Loc.t option +val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option +val local_binders_loc : local_binder_expr list -> Loc.t option (** {6 Constructors}*) @@ -48,10 +48,10 @@ val mkLambdaC : Name.t located list * binder_kind * 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 mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr +val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) -val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr +val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) (** @deprecated variant of mkCLambdaN *) |