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

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fb5927dbf7..0bb2979c2a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -184,13 +184,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env fix;
+        check_fix env ~chk:true fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env cofix;
+        check_cofix env ~chk:true cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop 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/typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 0bb2979c2a..fa6fd9677b 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -184,13 +184,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env ~chk:true fix;
+        check_fix env ~flags:{Declarations.check_guarded=true} fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env ~chk:true cofix;
+        check_cofix env ~flags:{Declarations.check_guarded=true} cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
-- 
cgit v1.2.3