diff options
| author | Maxime Dénès | 2017-05-25 11:16:35 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-25 11:16:35 +0200 |
| commit | f2fec63025d933f56dabf114a51720b1aae626c1 (patch) | |
| tree | 7f729302601fef48e6c59534a7904c7dfb92df2d /interp/constrexpr_ops.mli | |
| parent | 28f8da9489463b166391416de86420c15976522f (diff) | |
| parent | 94e783390ef9ad9d26a54add2287e0a3e58d1b70 (diff) | |
Merge PR#402: Uniform attribute handling in interfaces
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 b547288e3f..0ff51b060f 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 *) |