Add a field in `constant_body` to track constant whose well-foundedness is assumed.

4 files changed, 11 insertions, 7 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef3e1bb6a..591a7d404 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 870aef1d2..068bc498a 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 539305ed1..8a105ac97 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 a71587f0f..ba4d96a5f 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