Add a flag to deactivate guard checking in the kernel.

8 files changed, 47 insertions, 38 deletions

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c..358795666 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 4c1614bac..532287c30 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 5847d25f6..36f32b30c 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 48dbacf1a..9e9f18aaa 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 *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d48..efea4bec8 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 03fe2122c..d9f490ba5 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 fb5927dbf..0bb2979c2 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) ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6beaf54c5..06d7c629a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1168,7 +1168,7 @@ let do_program_recursive local p fixkind fixl ntns =
       in
       let indexes = 
 	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
-	List.iteri (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) fixl
+	List.iteri (fun i _ -> Inductive.check_fix env ~chk:true ((indexes,i),fixdecls)) fixl
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with