Add a comment making the spec of Inductiveops.mis_is_recursive more precise.

Author: ppedrot

pretyping/inductiveops.mli

@@ -63,8 +63,12 @@ val mkAppliedInd : inductive_type -> EConstr.constr
 val dest_recarg : recarg Rtree.Kind.t -> recarg
 val dest_subterms : recarg Rtree.Kind.t -> recarg Rtree.Kind.t array array
 
-(** Check if a [one_inductive_body] is recursive, possibly nestedly  *)
+(** Check if a [one_inductive_body] is recursive. An inductive is recursive
+    either if it has a constructor that mentions it in its normal form type, or
+    if it nested. Note that the latter case means that an inductive is
+    considered recursive even if the nesting type does not mention its argument. *)
 val mis_is_recursive : one_inductive_body -> bool
+
 val mis_is_nested : MutInd.t -> mutual_inductive_body -> bool
 val mis_nf_constructor_type :
   constructor puniverses -> mutual_inductive_body * one_inductive_body -> constr