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

1 files changed, 34 insertions, 34 deletions

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 8c14f5e045..32583f531b 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -326,7 +326,7 @@ let type_fixpoint env lna lar vdef vdeft =
     (* ATTENTION : faudra faire le typage du contexte des Const,
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
-let rec execute ~chkguard env cstr =
+let rec execute ~flags env cstr =
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
@@ -345,12 +345,12 @@ let rec execute ~chkguard env cstr =
       judge_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute ~chkguard env c in
+        let ct = execute ~flags env c in
           judge_of_projection env p c ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array ~chkguard env args in
+        let argst = execute_array ~flags env args in
 	let ft =
 	  match kind_of_term f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
@@ -363,7 +363,7 @@ let rec execute ~chkguard env cstr =
 	      judge_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* Full or no sort-polymorphism *)
-	    execute ~chkguard env f
+            execute ~flags env f
 	in
 
 	  judge_of_apply env f ft args argst
@@ -371,25 +371,25 @@ let rec execute ~chkguard env cstr =
     | Lambda (name,c1,c2) ->
       let _ = execute_is_type env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let c2t = execute ~chkguard env1 c2 in
+      let c2t = execute ~flags env1 c2 in
         judge_of_abstraction env name c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type ~chkguard env c1 in
+      let vars = execute_is_type ~flags env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let vars' = execute_is_type ~chkguard env1 c2 in
+      let vars' = execute_is_type ~flags env1 c2 in
 	judge_of_product env name vars vars'
 
     | LetIn (name,c1,c2,c3) ->
-      let c1t = execute ~chkguard env c1 in
+      let c1t = execute ~flags env c1 in
       let _c2s = execute_is_type env c2 in
       let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
       let env1 = push_rel (name,Some c1,c2) env in
-      let c3t = execute ~chkguard env1 c3 in
+      let c3t = execute ~flags env1 c3 in
 	subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute ~chkguard env c in
+      let ct = execute ~flags env c in
       let _ts = execute_type env t in
       let _ = judge_of_cast env c ct k t in
 	t
@@ -402,20 +402,20 @@ let rec execute ~chkguard env cstr =
       judge_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute ~chkguard env c in
-        let pt = execute ~chkguard env p in
-        let lft = execute_array ~chkguard env lf in
+        let ct = execute ~flags env c in
+        let pt = execute ~flags env p in
+        let lft = execute_array ~flags env lf in
           judge_of_case env ci p pt c ct lf lft
 
     | Fix ((vn,i as vni),recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
       let fix = (vni,recdef') in
-        check_fix env ~chk:chkguard fix; fix_ty
+        check_fix env ~flags fix; fix_ty
 	  
     | CoFix (i,recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env ~chk:chkguard cofix; fix_ty
+        check_cofix env ~flags cofix; fix_ty
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -424,41 +424,41 @@ let rec execute ~chkguard env cstr =
     | Evar _ ->
 	anomaly (Pp.str "the kernel does not support existential variables")
 
-and execute_is_type ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+and execute_is_type ~flags env constr =
+  let t = execute ~flags env constr in
     check_type env constr t
 
-and execute_type ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+and execute_type ~flags env constr =
+  let t = execute ~flags env constr in
     type_judgment env constr t
 
-and execute_recdef ~chkguard env (names,lar,vdef) i =
-  let lart = execute_array ~chkguard env lar in
+and execute_recdef ~flags env (names,lar,vdef) i =
+  let lart = execute_array ~flags env lar in
   let lara = Array.map2 (assumption_of_judgment env) lar lart in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdeft = execute_array ~chkguard env1 vdef in
+  let vdeft = execute_array ~flags env1 vdef in
   let () = type_fixpoint env1 names lara vdef vdeft in
     (lara.(i),(names,lara,vdef))
 
-and execute_array ~chkguard env = Array.map (execute ~chkguard env)
+and execute_array ~flags env = Array.map (execute ~flags env)
 
 (* Derived functions *)
-let infer ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+let infer ~flags env constr =
+  let t = execute ~flags env constr in
     make_judge constr t
 
 let infer = 
   if Flags.profile then
     let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c)
-  else (fun a b c -> infer ~chkguard:a b c)
+      Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c)
+  else (fun a b c -> infer ~flags:a b c)
 
 (* Restores the labels of [infer] lost to profiling. *)
-let infer ~chkguard env t = infer chkguard env t
+let infer ~flags env t = infer flags env t
 
-let infer_type ~chkguard env constr =
-  execute_type ~chkguard env constr
+let infer_type ~flags env constr =
+  execute_type ~flags env constr
 
-let infer_v ~chkguard env cv =
-  let jv = execute_array ~chkguard env cv in
+let infer_v ~flags env cv =
+  let jv = execute_array ~flags env cv in
     make_judgev cv jv