From d00472c59d15259b486868c5ccdb50b6e602a548 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Dec 2018 04:44:27 +0100
Subject: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.

This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.

p.s: Reading some comments was a lot of fun :)
---
 vernac/comInductive.ml | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'vernac/comInductive.ml')

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
-- 
cgit v1.2.3