diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8e9b606a5..1f2ae0b6c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( best-effort fashion. *) let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in - let recursive = finite != Decl_kinds.BiFinite in + let recursive = finite != BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let ra_env_ar = Array.rev_to_list rc in let nparamsctxt = Context.Rel.length paramsctxt in |