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.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.ml')
| -rw-r--r-- | interp/constrexpr.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 77d612cfd9..757d186c8b 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -80,8 +80,8 @@ type cases_pattern_expr_r = and cases_pattern_expr = cases_pattern_expr_r CAst.t and cases_pattern_notation_substitution = - cases_pattern_expr list * (** for constr subterms *) - cases_pattern_expr list list (** for recursive notations *) + cases_pattern_expr list * (* for constr subterms *) + cases_pattern_expr list list (* for recursive notations *) and constr_expr_r = | CRef of qualid * instance_expr option @@ -142,10 +142,10 @@ and local_binder_expr = | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t and constr_notation_substitution = - constr_expr list * (** for constr subterms *) - constr_expr list list * (** for recursive notations *) - cases_pattern_expr list * (** for binders *) - local_binder_expr list list (** for binder lists (recursive notations) *) + constr_expr list * (* for constr subterms *) + constr_expr list list * (* for recursive notations *) + cases_pattern_expr list * (* for binders *) + local_binder_expr list list (* for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr |