Add a flag to deactivate guard checking in the kernel.

3 files changed, 7 insertions, 7 deletions

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 =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 03fe2122c0..d9f490ba55 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs =
   if List.for_all is_singleton possible_indexes then
     let indexes = Array.of_list (List.map List.hd possible_indexes) in
     let fix = ((indexes, 0),fixdefs) in
-    (try check_fix env fix
+    (try check_fix env ~chk:true fix
      with reraise ->
        let (e, info) = Errors.push reraise in
        let info = Loc.add_loc info loc in
@@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs =
 	 (fun l ->
 	    let indexes = Array.of_list l in
 	    let fix = ((indexes, 0),fixdefs) in
-	    try check_fix env fix; raise (Found indexes)
+	    try check_fix env ~chk:true fix; raise (Found indexes)
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
@@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
-	    (try check_cofix env cofix
+	    (try check_cofix env ~chk:true cofix
              with reraise ->
                let (e, info) = Errors.push reraise in
                let info = Loc.add_loc info loc in
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) ->