From 576d7a815174106f337fca2f19ad7f26a7e87cc4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 26 Jun 2015 11:24:16 +0200
Subject: Add a flag to deactivate guard checking in the kernel.

---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d480..efea4bec89 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-	Inductive.check_cofix e cofix
+	Inductive.check_cofix ~chk:true e cofix
     | Fix (_,(_,_,_) as fix) ->
-	Inductive.check_fix e fix
+	Inductive.check_fix ~chk:true e fix
     | _ -> ()
   in
   let rec iter env c =
-- 
cgit v1.2.3


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
---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/inductiveops.ml')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index efea4bec89..930b0413e5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-	Inductive.check_cofix ~chk:true e cofix
+      Inductive.check_cofix ~flags:{check_guarded=true} e cofix
     | Fix (_,(_,_,_) as fix) ->
-	Inductive.check_fix ~chk:true e fix
+      Inductive.check_fix ~flags:{check_guarded=true} e fix
     | _ -> ()
   in
   let rec iter env c =
-- 
cgit v1.2.3