Add a flag to deactivate guard checking in the kernel.

4 files changed, 39 insertions, 30 deletions

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c6..358795666d 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -410,12 +410,12 @@ let rec execute env cstr =
     | Fix ((vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
-        check_fix env fix; fix_ty
+        check_fix env ~chk:true fix; fix_ty
 	  
     | CoFix (i,recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env cofix; fix_ty
+        check_cofix env ~chk:true cofix; fix_ty
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4c1614bac1..532287c304 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1065,21 +1065,24 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
-  let (minds, rdef) = inductive_of_mutfix env fix in
-  let get_tree (kn,i) =
-    let mib = Environ.lookup_mind kn env in
-    mib.mind_packets.(i).mind_recargs
-  in
-  let trees = Array.map (fun (mind,_) -> get_tree mind) minds in
-  for i = 0 to Array.length bodies - 1 do
-    let (fenv,body) = rdef.(i) in
-    let renv = make_renv fenv nvect.(i) trees.(i) in
-    try check_one_fix renv nvect trees body
-    with FixGuardError (fixenv,err) ->
-      error_ill_formed_rec_body fixenv err names i
-	(push_rec_types recdef env) (judgment_of_fixpoint recdef)
-  done
+let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) =
+  if chk then
+    let (minds, rdef) = inductive_of_mutfix env fix in
+    let get_tree (kn,i) =
+      let mib = Environ.lookup_mind kn env in
+      mib.mind_packets.(i).mind_recargs
+    in
+    let trees = Array.map (fun (mind,_) -> get_tree mind) minds in
+    for i = 0 to Array.length bodies - 1 do
+      let (fenv,body) = rdef.(i) in
+      let renv = make_renv fenv nvect.(i) trees.(i) in
+      try check_one_fix renv nvect trees body
+      with FixGuardError (fixenv,err) ->
+        error_ill_formed_rec_body fixenv err names i
+	  (push_rec_types recdef env) (judgment_of_fixpoint recdef)
+    done
+  else
+    ()
 
 (*
 let cfkey = Profile.declare_profile "check_fix";;
@@ -1190,12 +1193,15 @@ 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 (bodynum,(names,types,bodies as recdef)) =
-  let nbfix = Array.length bodies in
-  for i = 0 to nbfix-1 do
-    let fixenv = push_rec_types recdef env in
-    try check_one_cofix fixenv nbfix bodies.(i) types.(i)
-    with CoFixGuardError (errenv,err) ->
-      error_ill_formed_rec_body errenv err names i
-	fixenv (judgment_of_fixpoint recdef)
-  done
+let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) =
+  if chk then
+    let nbfix = Array.length bodies in
+    for i = 0 to nbfix-1 do
+      let fixenv = push_rec_types recdef env in
+      try check_one_cofix fixenv nbfix bodies.(i) types.(i)
+      with CoFixGuardError (errenv,err) ->
+        error_ill_formed_rec_body errenv err names i
+	  fixenv (judgment_of_fixpoint recdef)
+    done
+  else
+    ()
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 5847d25f6f..36f32b30c6 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -95,8 +95,11 @@ val inductive_sort_family : one_inductive_body -> sorts_family
 val check_case_info : env -> pinductive -> case_info -> unit
 
 (** {6 Guard conditions for fix and cofix-points. } *)
-val check_fix : env -> fixpoint -> unit
-val check_cofix : env -> cofixpoint -> unit
+
+(** When [chk] is false, the guard condition is not actually
+    checked. *)
+val check_fix : env -> chk:bool -> fixpoint -> unit
+val check_cofix : env -> chk:bool -> cofixpoint -> unit
 
 (** {6 Support for sort-polymorphic inductive types } *)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1a4..9e9f18aaa9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -494,13 +494,13 @@ let rec execute env cstr =
     | Fix ((vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
-        check_fix env fix;
+        check_fix ~chk:true env fix;
 	make_judge (mkFix fix) fix_ty
 	  
     | CoFix (i,recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env cofix;
+        check_cofix ~chk:true env cofix;
 	(make_judge (mkCoFix cofix) fix_ty)
 	  
     (* Partial proofs: unsupported by the kernel *)