From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 7 Jun 2016 09:52:43 +0200
Subject: Assume totality: dedicated type rather than bool

The rational is that

1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
---
 kernel/inductive.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 532287c304..fdca5ce26b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1065,8 +1065,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) =
-  if chk then
+let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) =
+  if flags.check_guarded then
     let (minds, rdef) = inductive_of_mutfix env fix in
     let get_tree (kn,i) =
       let mib = Environ.lookup_mind kn env in
@@ -1193,8 +1193,8 @@ let check_one_cofix env nbfix def deftype =
 (* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)
 
-let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) =
-  if chk then
+let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) =
+  if flags.check_guarded then
     let nbfix = Array.length bodies in
     for i = 0 to nbfix-1 do
       let fixenv = push_rec_types recdef env in
-- 
cgit v1.2.3