diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /interp/constrexpr_ops.ml | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3a4969a3ee..3a5af1dd5f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 = in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> - (** Don't care about the case_style *) + (* Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 @@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) + (* Don't care about the [binder_kind] *) List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) (** Folds and maps *) - let is_constructor id = try Globnames.isConstructRef (Smartlocate.global_of_extended_global |
