From 8589b9b487c1e9b996975bd5dc58f548d0d9280c Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 22 Jun 2015 13:42:13 +0200
Subject: Add a field in `mutual_inductive_body` to represent mutual inductive
 whose positivity is assumed.

---
 kernel/declarations.mli | 1 +
 kernel/declareops.ml    | 4 +++-
 kernel/indtypes.ml      | 1 +
 3 files changed, 5 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3f0..ef3e1bb6ae 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -184,6 +184,7 @@ type mutual_inductive_body = {
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
   
+    mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
 }
 
 (** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c13..870aef1d28 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -258,7 +258,9 @@ let subst_mind_body sub mib =
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
-    mind_private = mib.mind_private }
+    mind_private = mib.mind_private;
+    mind_checked_positive = mib.mind_checked_positive;
+  }
 
 let inductive_instance mib =
   if mib.mind_polymorphic then
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 92e121402a..72b615cc89 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -857,6 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       mind_polymorphic = p;
       mind_universes = ctx;
       mind_private = prv;
+      mind_checked_positive = true;
     }
 
 (************************************************************************)
-- 
cgit v1.2.3


From 9a1e80524e1650311b019fedbd7e774242d80ea4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 09:24:43 +0200
Subject: Add a corresponding field in `mutual_inductive_entry` (part 1).

The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
---
 kernel/entries.mli | 5 ++++-
 kernel/indtypes.ml | 6 +++---
 2 files changed, 7 insertions(+), 4 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 303d27d355..1a27aa9f6a 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -51,7 +51,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
-  mind_entry_private : bool option }
+  mind_entry_private : bool option;
+  mind_entry_check_positivity : bool;
+  (** [false] if positivity is to be assumed. *)
+}
 
 (** {6 Constants (Definition/Axiom) } *)
 type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 72b615cc89..620c0f6d80 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -752,7 +752,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
-let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs =
+let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs is_checked =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
@@ -857,7 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       mind_polymorphic = p;
       mind_universes = ctx;
       mind_private = prv;
-      mind_checked_positive = true;
+      mind_checked_positive = is_checked;
     }
 
 (************************************************************************)
@@ -872,4 +872,4 @@ let check_inductive env kn mie =
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
       env_ar params kn mie.mind_entry_record mie.mind_entry_finite
-      inds nmr recargs
+      inds nmr recargs mie.mind_entry_check_positivity
-- 
cgit v1.2.3


From 4a73e6b2bfb75451bcda7c74cf7478726a459799 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 15:44:31 +0200
Subject: Add a corresponding field in `mutual_inductive_entry` (part 2).

The request for positivity to be assumed is honored.
---
 kernel/indtypes.ml | 46 +++++++++++++++++++++++++++++++---------------
 1 file changed, 31 insertions(+), 15 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 620c0f6d80..3516d4ef65 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -480,8 +480,12 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
     for use by the guard condition (terms at these positions are
     considered sub-terms) as well as the number of of non-uniform
     arguments (used to generate induction schemes, so a priori less
-    relevant to the kernel). *)
-let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
+    relevant to the kernel).
+
+    If [chkpos] is [false] then positivity is assumed, and
+    [check_positivity_one] computes the subterms occurrences in a
+    best-effort fashion. *)
+let check_positivity_one ~chkpos (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
   let lparams = rel_context_length hyps in
   let nmr = rel_context_nhyps hyps in
   (** Positivity of one argument [c] of a constructor (i.e. the
@@ -498,9 +502,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
                 recursive call. Occurrences in the right-hand side of
                 the product must be strictly positive.*)
             (match weaker_noccur_between env n ntypes b with
-		None -> failwith_non_pos_list n ntypes [b]
+	      | None when chkpos ->
+                  failwith_non_pos_list n ntypes [b]
+              | None ->
+                  check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d
               | Some b ->
-	          check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
+                  check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
 	| Rel k ->
             (try let (ra,rarg) = List.nth ra_env (k-1) in
             let largs = List.map (whd_betadeltaiota env) largs in
@@ -512,7 +519,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
               (** The case where one of the inductives of the mutually
                   inductive block occurs as an argument of another is not
                   known to be safe. So Coq rejects it. *)
-	      if not (List.for_all (noccur_between n ntypes) largs)
+	      if chkpos &&
+                 not (List.for_all (noccur_between n ntypes) largs)
 	      then failwith_non_pos_list n ntypes largs
 	      else (nmr1,rarg)
               with Failure _ | Invalid_argument _ -> (nmr,mk_norec))
@@ -527,8 +535,9 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
             (** If an inductive of the mutually inductive block
                 appears in any other way, then the positivy check gives
                 up. *)
-	    if noccur_between n ntypes x &&
-              List.for_all (noccur_between n ntypes) largs
+	    if not chkpos ||
+              (noccur_between n ntypes x &&
+               List.for_all (noccur_between n ntypes) largs)
 	    then (nmr,mk_norec)
 	    else failwith_non_pos_list n ntypes (x::largs)
 
@@ -550,7 +559,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
       (** Inductives of the inductive block being defined are only
           allowed to appear nested in the parameters of another inductive
           type. Not in the proper indices. *)
-      if not (List.for_all (noccur_between n ntypes) auxlargs) then
+      if chkpos &&
+         not (List.for_all (noccur_between n ntypes) auxlargs) then
 	failwith_non_pos_list n ntypes auxlargs;
       (* Nested mutual inductive types are not supported *)
       let auxntyp = mib.mind_ntypes in
@@ -608,7 +618,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
                 | _ -> raise (IllFormedInd LocalNotConstructor)
                 end
               else
-                if not (List.for_all (noccur_between n ntypes) largs)
+                if chkpos &&
+                   not (List.for_all (noccur_between n ntypes) largs)
                 then failwith_non_pos_list n ntypes largs
             in
             (nmr, List.rev lrec)
@@ -628,9 +639,13 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
   and nmr' = array_min nmr irecargs_nmr
   in (nmr', mk_paths (Mrec ind) irecargs)
 
-(** [check_positivity kn env_ar params] checks that the mutually
-    inductive block [inds] is strictly positive. *)
-let check_positivity kn env_ar params inds =
+(** [check_positivity ~chkpos kn env_ar params] checks that the mutually
+    inductive block [inds] is strictly positive.
+
+    If [chkpos] is [false] then positivity is assumed, and
+    [check_positivity_one] computes the subterms occurrences in a
+    best-effort fashion. *)
+let check_positivity ~chkpos kn env_ar params inds =
   let ntypes = Array.length inds in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
@@ -641,7 +656,7 @@ let check_positivity kn env_ar params inds =
       List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = rel_context_nhyps sign - nmr in
-    check_positivity_one ienv params (kn,i) nargs lcnames lc
+    check_positivity_one ~chkpos ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
   let irecargs = Array.map snd irecargs_nmr
@@ -866,10 +881,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
+  let chkpos = mie.mind_entry_check_positivity in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
+  let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par params inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
       env_ar params kn mie.mind_entry_record mie.mind_entry_finite
-      inds nmr recargs mie.mind_entry_check_positivity
+      inds nmr recargs chkpos
-- 
cgit v1.2.3


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.

---
 kernel/fast_typeops.ml |  4 ++--
 kernel/inductive.ml    | 54 ++++++++++++++++++++++++++++----------------------
 kernel/inductive.mli   |  7 +++++--
 kernel/typeops.ml      |  4 ++--
 4 files changed, 39 insertions(+), 30 deletions(-)

(limited to 'kernel')

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 *)
-- 
cgit v1.2.3


From e8bad8abc7be351a34fdf9770409bbab14bcd6a9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 24 Jul 2015 08:46:09 +0200
Subject: Propagate `Guarded` flag from syntax to kernel.

The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
---
 kernel/fast_typeops.ml  | 69 ++++++++++++++++++++++++++-----------------------
 kernel/fast_typeops.mli |  6 ++---
 kernel/safe_typing.ml   | 13 +++++-----
 kernel/safe_typing.mli  |  4 ++-
 kernel/term_typing.ml   | 28 ++++++++++----------
 kernel/term_typing.mli  |  8 +++---
 6 files changed, 67 insertions(+), 61 deletions(-)

(limited to 'kernel')

diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 358795666d..8c14f5e045 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 env cstr =
+let rec execute ~chkguard env cstr =
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
@@ -345,12 +345,12 @@ let rec execute env cstr =
       judge_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute env c in
+        let ct = execute ~chkguard env c in
           judge_of_projection env p c ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array env args in
+        let argst = execute_array ~chkguard 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 env cstr =
 	      judge_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* Full or no sort-polymorphism *)
-	    execute env f
+	    execute ~chkguard env f
 	in
 
 	  judge_of_apply env f ft args argst
@@ -371,25 +371,25 @@ let rec execute 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 env1 c2 in
+      let c2t = execute ~chkguard env1 c2 in
         judge_of_abstraction env name c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type env c1 in
+      let vars = execute_is_type ~chkguard env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let vars' = execute_is_type env1 c2 in
+      let vars' = execute_is_type ~chkguard env1 c2 in
 	judge_of_product env name vars vars'
 
     | LetIn (name,c1,c2,c3) ->
-      let c1t = execute env c1 in
+      let c1t = execute ~chkguard 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 env1 c3 in
+      let c3t = execute ~chkguard env1 c3 in
 	subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute env c in
+      let ct = execute ~chkguard 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 env cstr =
       judge_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute env c in
-        let pt = execute env p in
-        let lft = execute_array env lf in
+        let ct = execute ~chkguard env c in
+        let pt = execute ~chkguard env p in
+        let lft = execute_array ~chkguard 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 env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
       let fix = (vni,recdef') in
-        check_fix env ~chk:true fix; fix_ty
+        check_fix env ~chk:chkguard fix; fix_ty
 	  
     | CoFix (i,recdef) ->
-      let (fix_ty,recdef') = execute_recdef env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env ~chk:true cofix; fix_ty
+        check_cofix env ~chk:chkguard cofix; fix_ty
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -424,38 +424,41 @@ let rec execute env cstr =
     | Evar _ ->
 	anomaly (Pp.str "the kernel does not support existential variables")
 
-and execute_is_type env constr =
-  let t = execute env constr in
+and execute_is_type ~chkguard env constr =
+  let t = execute ~chkguard env constr in
     check_type env constr t
 
-and execute_type env constr =
-  let t = execute env constr in
+and execute_type ~chkguard env constr =
+  let t = execute ~chkguard env constr in
     type_judgment env constr t
 
-and execute_recdef env (names,lar,vdef) i =
-  let lart = execute_array env lar in
+and execute_recdef ~chkguard env (names,lar,vdef) i =
+  let lart = execute_array ~chkguard 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 env1 vdef in
+  let vdeft = execute_array ~chkguard env1 vdef in
   let () = type_fixpoint env1 names lara vdef vdeft in
     (lara.(i),(names,lara,vdef))
 
-and execute_array env = Array.map (execute env)
+and execute_array ~chkguard env = Array.map (execute ~chkguard env)
 
 (* Derived functions *)
-let infer env constr =
-  let t = execute env constr in
+let infer ~chkguard env constr =
+  let t = execute ~chkguard env constr in
     make_judge constr t
 
 let infer = 
   if Flags.profile then
     let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile2 infer_key infer
-  else infer
+      Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c)
+  else (fun a b c -> infer ~chkguard:a b c)
 
-let infer_type env constr =
-  execute_type env constr
+(* Restores the labels of [infer] lost to profiling. *)
+let infer ~chkguard env t = infer chkguard env t
 
-let infer_v env cv =
-  let jv = execute_array env cv in
+let infer_type ~chkguard env constr =
+  execute_type ~chkguard env constr
+
+let infer_v ~chkguard env cv =
+  let jv = execute_array ~chkguard env cv in
     make_judgev cv jv
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 90d9c55f16..98dbefad13 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -18,6 +18,6 @@ open Environ
  *)
 
 
-val infer      : env -> constr       -> unsafe_judgment
-val infer_v    : env -> constr array -> unsafe_judgment array
-val infer_type : env -> types        -> unsafe_type_judgment
+val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
+val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
+val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d9adca0c91..18d8978174 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 
-let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
+let push_named_def ~chkguard (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in
   let senv' = push_context univs senv in
   let c, senv' = match c with
     | Def c -> Mod_subst.force_constr c, senv'
@@ -346,9 +346,9 @@ let push_named_def (id,de) senv =
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
-let push_named_assum ((id,t),ctx) senv =
+let push_named_assum ~chkguard ((id,t),ctx) senv =
   let senv' = push_context_set ctx senv in
-  let t = Term_typing.translate_local_assum senv'.env t in
+  let t = Term_typing.translate_local_assum ~chkguard senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
 
@@ -439,13 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+  | ConstantEntry of Entries.constant_entry * bool (* check guard *)
   | GlobalRecipe of Cooking.recipe
 
 let add_constant dir l decl senv =
   let kn = make_con senv.modpath dir l in
   let cb = match decl with
-    | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
+    | ConstantEntry (ce,chkguard) ->
+        Term_typing.translate_constant ~chkguard senv.env kn ce
     | GlobalRecipe r ->
       let cb = Term_typing.translate_recipe senv.env kn r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a57fb108c4..80b9bb495a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,14 +57,16 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
+  chkguard:bool ->
   (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
 val push_named_def :
+  chkguard:bool ->
   Id.t * Entries.definition_entry -> safe_transformer0
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+  | ConstantEntry of Entries.constant_entry * bool (* chkguard *)
   | GlobalRecipe of Cooking.recipe
 
 val add_constant :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492b..539305ed13 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,18 +23,18 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type env j poly subst = function
+let constrain_type ~chkguard env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
       make_polymorphic_if_constant_for_ind env j
     else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
   | `Some t ->
-      let tj = infer_type env t in
+      let tj = infer_type ~chkguard env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
   | `SomeWJ (t, tj) ->
-      let tj = infer_type env t in
+      let tj = infer_type ~chkguard env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
@@ -101,11 +101,11 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 
-let infer_declaration env kn dcl =
+let infer_declaration ~chkguard env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context uctx env in
-      let j = infer env t in
+      let j = infer ~chkguard env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
       let c = Typeops.assumption_of_judgment env j in
@@ -122,7 +122,7 @@ let infer_declaration env kn dcl =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
           let body = handle_side_effects env body side_eff in
 	  let env' = push_context_set ctx env in
-          let j = infer env' body in
+          let j = infer ~chkguard env' body in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
@@ -143,8 +143,8 @@ let infer_declaration env kn dcl =
       let body = handle_side_effects env body side_eff in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
-      let j = infer env body in
-      let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let j = infer ~chkguard env body in
+      let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -266,20 +266,20 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 
 (*s Global and local constant declaration. *)
 
-let translate_constant env kn ce =
-  build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant ~chkguard env kn ce =
+  build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce)
 
-let translate_local_assum env t =
-  let j = infer env t in
+let translate_local_assum ~chkguard env t =
+  let j = infer ~chkguard env t in
   let t = Typeops.assumption_of_judgment env j in
     t
 
 let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant env r)
 
-let translate_local_def env id centry =
+let translate_local_def ~chkguard env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration env None (DefinitionEntry centry) in
+    infer_declaration ~chkguard env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   def, typ, univs
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea1e..a71587f0fb 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,10 +12,10 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry ->
   constant_def * types * constant_universes
 
-val translate_local_assum : env -> types -> types
+val translate_local_assum : chkguard:bool -> env -> types -> types
 
 val mk_pure_proof : constr -> proof_output
 
@@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,7 +37,7 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : env -> constant option -> 
+val infer_declaration : chkguard:bool -> env -> constant option -> 
   constant_entry -> Cooking.result
 
 val build_constant_declaration :
-- 
cgit v1.2.3


From caf8402e4af75d85223e10cba68a6a145e050dab Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Sep 2015 15:09:15 +0200
Subject: Add a field in `constant_body` to track constant whose
 well-foundedness is assumed.

---
 kernel/declarations.mli | 4 +++-
 kernel/declareops.ml    | 3 ++-
 kernel/term_typing.ml   | 9 +++++----
 kernel/term_typing.mli  | 2 +-
 4 files changed, 11 insertions(+), 7 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef3e1bb6ae..591a7d404c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -74,7 +74,9 @@ type constant_body = {
     const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
-    const_inline_code : bool }
+    const_inline_code : bool;
+    const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *)
+}
 
 type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 870aef1d28..068bc498a0 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -132,7 +132,8 @@ let subst_const_body sub cb =
           Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
-        const_inline_code = cb.const_inline_code }
+        const_inline_code = cb.const_inline_code;
+        const_checked_guarded = cb.const_checked_guarded }
 
 (** {7 Hash-consing of constants } *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 539305ed13..8a105ac971 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -186,7 +186,7 @@ let record_aux env s1 s2 =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -261,13 +261,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_body_code = tps;
     const_polymorphic = poly;
     const_universes = univs;
-    const_inline_code = inline_code }
+    const_inline_code = inline_code;
+    const_checked_guarded = chkguard }
 
 
 (*s Global and local constant declaration. *)
 
 let translate_constant ~chkguard env kn ce =
-  build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce)
+  build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce)
 
 let translate_local_assum ~chkguard env t =
   let j = infer ~chkguard env t in
@@ -275,7 +276,7 @@ let translate_local_assum ~chkguard env t =
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant env r)
+  build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r)
 
 let translate_local_def ~chkguard env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index a71587f0fb..ba4d96a5f0 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -41,7 +41,7 @@ val infer_declaration : chkguard:bool -> env -> constant option ->
   constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  constant -> env -> Cooking.result -> constant_body
+  chkguard:bool -> constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
   (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
-- 
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
---
 kernel/declarations.mli | 13 +++++++++-
 kernel/declareops.ml    |  2 +-
 kernel/fast_typeops.ml  | 68 ++++++++++++++++++++++++-------------------------
 kernel/fast_typeops.mli |  7 ++---
 kernel/inductive.ml     |  8 +++---
 kernel/inductive.mli    |  4 +--
 kernel/safe_typing.ml   | 14 +++++-----
 kernel/safe_typing.mli  |  6 ++---
 kernel/term_typing.ml   | 34 ++++++++++++-------------
 kernel/term_typing.mli  | 10 ++++----
 kernel/typeops.ml       |  4 +--
 11 files changed, 91 insertions(+), 79 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 591a7d404c..0c085df39e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -64,6 +64,15 @@ type constant_def =
 
 type constant_universes = Univ.universe_context
 
+(** The [typing_flags] are instructions to the type-checker which
+    modify its behaviour. The typing flags used in the type-checking
+    of a constant are tracked in their {!constant_body} so that they
+    can be displayed to the user. *)
+type typing_flags = {
+  check_guarded : bool; (** If [false] then fixed points and co-fixed
+                            points are assumed to be total. *)
+}
+
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
 type constant_body = {
@@ -75,7 +84,9 @@ type constant_body = {
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
-    const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *)
+    const_typing_flags : typing_flags; (** The typing options which
+                                           were used for
+                                           type-checking. *)
 }
 
 type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 068bc498a0..98d2877373 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -133,7 +133,7 @@ let subst_const_body sub cb =
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code;
-        const_checked_guarded = cb.const_checked_guarded }
+        const_typing_flags = cb.const_typing_flags }
 
 (** {7 Hash-consing of constants } *)
 
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
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 98dbefad13..1c0146baea 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Environ
+open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     
@@ -18,6 +19,6 @@ open Environ
  *)
 
 
-val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
-val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
-val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
+val infer      : flags:typing_flags -> env -> constr       -> unsafe_judgment
+val infer_v    : flags:typing_flags -> env -> constr array -> unsafe_judgment array
+val infer_type : flags:typing_flags -> env -> types        -> unsafe_type_judgment
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 532287c304..fdca5ce26b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1065,8 +1065,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) =
-  if chk then
+let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) =
+  if flags.check_guarded then
     let (minds, rdef) = inductive_of_mutfix env fix in
     let get_tree (kn,i) =
       let mib = Environ.lookup_mind kn env in
@@ -1193,8 +1193,8 @@ 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 ~chk (bodynum,(names,types,bodies as recdef)) =
-  if chk then
+let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) =
+  if flags.check_guarded then
     let nbfix = Array.length bodies in
     for i = 0 to nbfix-1 do
       let fixenv = push_rec_types recdef env in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 36f32b30c6..54036d86aa 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -98,8 +98,8 @@ val check_case_info : env -> pinductive -> case_info -> 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
+val check_fix : env -> flags:typing_flags -> fixpoint -> unit
+val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit
 
 (** {6 Support for sort-polymorphic inductive types } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 18d8978174..2cea50d9ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 
-let push_named_def ~chkguard (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in
+let push_named_def ~flags (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def ~flags senv.env id de in
   let senv' = push_context univs senv in
   let c, senv' = match c with
     | Def c -> Mod_subst.force_constr c, senv'
@@ -346,9 +346,9 @@ let push_named_def ~chkguard (id,de) senv =
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
-let push_named_assum ~chkguard ((id,t),ctx) senv =
+let push_named_assum ~flags ((id,t),ctx) senv =
   let senv' = push_context_set ctx senv in
-  let t = Term_typing.translate_local_assum ~chkguard senv'.env t in
+  let t = Term_typing.translate_local_assum ~flags senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
 
@@ -439,14 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry * bool (* check guard *)
+  | ConstantEntry of Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 let add_constant dir l decl senv =
   let kn = make_con senv.modpath dir l in
   let cb = match decl with
-    | ConstantEntry (ce,chkguard) ->
-        Term_typing.translate_constant ~chkguard senv.env kn ce
+    | ConstantEntry (ce,flags) ->
+        Term_typing.translate_constant ~flags senv.env kn ce
     | GlobalRecipe r ->
       let cb = Term_typing.translate_recipe senv.env kn r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 80b9bb495a..c5e43e42ac 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
 val push_named_def :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   Id.t * Entries.definition_entry -> safe_transformer0
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry * bool (* chkguard *)
+  | ConstantEntry of Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 val add_constant :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8a105ac971..64597469a8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,18 +23,18 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type ~chkguard env j poly subst = function
+let constrain_type ~flags env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
       make_polymorphic_if_constant_for_ind env j
     else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
   | `Some t ->
-      let tj = infer_type ~chkguard env t in
+      let tj = infer_type ~flags env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
   | `SomeWJ (t, tj) ->
-      let tj = infer_type ~chkguard env t in
+      let tj = infer_type ~flags env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
@@ -101,11 +101,11 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 
-let infer_declaration ~chkguard env kn dcl =
+let infer_declaration ~flags env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context uctx env in
-      let j = infer ~chkguard env t in
+      let j = infer ~flags env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
       let c = Typeops.assumption_of_judgment env j in
@@ -122,7 +122,7 @@ let infer_declaration ~chkguard env kn dcl =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
           let body = handle_side_effects env body side_eff in
 	  let env' = push_context_set ctx env in
-          let j = infer ~chkguard env' body in
+          let j = infer ~flags env' body in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
@@ -143,8 +143,8 @@ let infer_declaration ~chkguard env kn dcl =
       let body = handle_side_effects env body side_eff in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
-      let j = infer ~chkguard env body in
-      let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let j = infer ~flags env body in
+      let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -186,7 +186,7 @@ let record_aux env s1 s2 =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -262,25 +262,25 @@ let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_
     const_polymorphic = poly;
     const_universes = univs;
     const_inline_code = inline_code;
-    const_checked_guarded = chkguard }
+    const_typing_flags = flags }
 
 
 (*s Global and local constant declaration. *)
 
-let translate_constant ~chkguard env kn ce =
-  build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce)
+let translate_constant ~flags env kn ce =
+  build_constant_declaration ~flags kn env (infer_declaration ~flags env (Some kn) ce)
 
-let translate_local_assum ~chkguard env t =
-  let j = infer ~chkguard env t in
+let translate_local_assum ~flags env t =
+  let j = infer ~flags env t in
   let t = Typeops.assumption_of_judgment env j in
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r)
+  build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r)
 
-let translate_local_def ~chkguard env id centry =
+let translate_local_def ~flags env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration ~chkguard env None (DefinitionEntry centry) in
+    infer_declaration ~flags env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   def, typ, univs
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ba4d96a5f0..f167603a79 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,10 +12,10 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry ->
+val translate_local_def : flags:typing_flags -> env -> Id.t -> definition_entry ->
   constant_def * types * constant_universes
 
-val translate_local_assum : chkguard:bool -> env -> types -> types
+val translate_local_assum : flags:typing_flags -> env -> types -> types
 
 val mk_pure_proof : constr -> proof_output
 
@@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body
+val translate_constant : flags:typing_flags -> env -> constant -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,11 +37,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : chkguard:bool -> env -> constant option -> 
+val infer_declaration : flags:typing_flags -> env -> constant option ->
   constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  chkguard:bool -> constant -> env -> Cooking.result -> constant_body
+  flags:typing_flags -> constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
   (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9e9f18aaa9..1c3117725c 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 ~chk:true env fix;
+        check_fix ~flags:{check_guarded=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 ~chk:true env cofix;
+        check_cofix ~flags:{check_guarded=true} env cofix;
 	(make_judge (mkCoFix cofix) fix_ty)
 	  
     (* Partial proofs: unsupported by the kernel *)
-- 
cgit v1.2.3