Fixing the checker.

This is a stupid fix that only allows to take into account the change in
memory layout. The check will simply fail when encountering a unguarded
inductive or (co)fixpoint.

1 files changed, 12 insertions, 1 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 82eb35bcb..cac2384fc 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -208,6 +208,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. *)
+}
+
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
@@ -216,7 +225,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_typing_flags : typing_flags;
+}
 
 (** {6 Representation of mutual inductive types } *)