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 /vernac/comInductive.ml | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'vernac/comInductive.ml')
| -rw-r--r-- | vernac/comInductive.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8b9cf7d269..4af6415a4d 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -265,7 +265,7 @@ let inductive_levels env evd poly arities inds = else minlev in let minlev = - (** Indices contribute. *) + (* Indices contribute. *) if indices_matter env && List.length ctx > 0 then ( let ilev = sign_level env evd ctx in Univ.sup ilev minlev) @@ -282,15 +282,15 @@ let inductive_levels env evd poly arities inds = let evd, arities = CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then - (** Any product is allowed here. *) + (* Any product is allowed here. *) evd, arity :: arities - else (** If in a predicative sort, or asked to infer the type, - we take the max of: - - indices (if in indices-matter mode) - - constructors - - Type(1) if there is more than 1 constructor + else (* If in a predicative sort, or asked to infer the type, + we take the max of: + - indices (if in indices-matter mode) + - constructors + - Type(1) if there is more than 1 constructor *) - (** Constructors contribute. *) + (* Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then @@ -301,7 +301,7 @@ let inductive_levels env evd poly arities inds = in let evd = if len >= 2 && Univ.is_type0m_univ cu then - (** "Polymorphic" type constraint and more than one constructor, + (* "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd Set du @@ -510,7 +510,7 @@ let is_recursive mie = let rec is_recursive_constructor lift typ = match Constr.kind typ with | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || + not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || is_recursive_constructor (lift+1) rest | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest | _ -> false |