Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.

9 files changed, 100 insertions, 58 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 1802b2d36..c05c5f6c2 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -286,11 +286,17 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
     if is_local_assum decl then ContextObjectMap.add (Variable id) t accu
     else accu
   | ConstRef kn ->
-    let cb = lookup_constant kn in
+      let cb = lookup_constant kn in
+      let accu =
+        if cb.const_typing_flags.check_guarded then accu
+        else
+          let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
+      in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
       let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
-      ContextObjectMap.add (Axiom (kn,l)) t accu
+      ContextObjectMap.add (Axiom (Constant kn,l)) t accu
     else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Opaque kn) t accu
@@ -299,6 +305,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       ContextObjectMap.add (Transparent kn) t accu
     else
       accu
-  | IndRef _ | ConstructRef _ -> accu
+  | IndRef (m,_) | ConstructRef ((m,_),_) ->
+      let mind = Global.lookup_mind m in
+      if mind.mind_checked_positive then
+        accu
+      else
+        let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+        ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
   in
   Refmap_env.fold fold graph ContextObjectMap.empty
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f0f678e08..6f2dd1bf1 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -145,9 +145,9 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ident ce local k pl imps =
+let declare_global_definition ~flags ident ce local k pl imps =
   let local = get_locality ident local in
-  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+  let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Universes.register_universe_binders gr pl in
@@ -158,7 +158,7 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ident (local, p, k) ce pl imps hook =
+let declare_definition ~flags ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
@@ -175,11 +175,11 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ident ce local k pl imps in
+    declare_global_definition ~flags ident ce local k pl imps in
   Lemmas.call_hook fix_exn hook local r
 
 let _ = Obligations.declare_definition_ref :=
-       (fun i k c imps hook -> declare_definition i k c [] imps hook)
+       (fun i k c imps hook -> declare_definition ~flags:{Declarations.check_guarded=true} i k c [] imps hook)
 
 let do_definition ident k pl bl red_option c ctypopt hook =
   let (ce, evd, pl', imps as def) =
@@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ident k ce pl' imps
+      ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -549,7 +549,7 @@ let check_param = function
 | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
 | LocalRawAssum (nas, Generalized _, _) -> ()
 
-let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
+let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
@@ -630,7 +630,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = uctx },
+    mind_entry_universes = uctx;
+    mind_entry_check_positivity = chk; },
     pl, impls
 
 (* Very syntactical equality *)
@@ -715,17 +716,20 @@ type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)
 
-let do_mutual_inductive indl poly prv finite =
+let do_mutual_inductive chk indl poly prv finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive chk indl ntns poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes
-	    
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
+  (* If [chk] is [false] (i.e. positivity is assumed) declares itself
+     as unsafe. *)
+  if not chk then Feedback.feedback Feedback.AddedAxiom else ()
+
 (* 3c| Fixpoints and co-fixpoints *)
 
 (* An (unoptimized) function that maps preorders to partial orders...
@@ -829,12 +833,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
+let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref :=
-	  (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
+  (fun ?opaque k ctx f d t imps -> declare_fix ~flags:{Declarations.check_guarded=true} ?opaque k [] ctx f d t imps)
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1135,7 +1139,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   (fix,pl,Evd.evar_universe_context evd,info)
     
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1155,7 +1159,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let env = Global.env() in
-    let indexes = search_guard Loc.ghost env indexes fixdecls in
+    let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
@@ -1164,7 +1168,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let evd = Evd.restrict_universe_context evd vars in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
+    ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1172,7 +1176,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1198,7 +1202,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
+    ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1264,8 +1268,14 @@ let do_program_recursive local p fixkind fixl ntns =
 	Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
       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
+        Pretyping.search_guard
+          ~tflags:{Declarations.check_guarded=true}
+          Loc.ghost (Global.env ()) possible_indexes fixdecls in
+      List.iteri (fun i _ ->
+          Inductive.check_fix env
+                              ~flags:{Declarations.check_guarded=true}
+                              ((indexes,i),fixdecls))
+        fixl
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
@@ -1299,19 +1309,21 @@ let do_program_fixpoint local poly l =
 	errorlabstrm "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_fixpoint local poly l =
+let do_fixpoint ~flags local poly l =
   if Flags.is_program_mode () then do_program_fixpoint local poly l
   else
     let fixl, ntns = extract_fixpoint_components true l in
     let (_, _, _, info as fix) = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences info in
-    declare_fixpoint local poly fix possible_indexes ntns
+    declare_fixpoint ~flags local poly fix possible_indexes ntns;
+    if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~flags local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
     if Flags.is_program_mode () then
       do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-	declare_cofixpoint local poly cofix ntns
+      declare_cofixpoint ~flags local poly cofix ntns;
+      if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b97cb487d..2d27552a1 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,7 +36,7 @@ val interp_definition :
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
-val declare_definition : Id.t -> definition_kind ->
+val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind ->
   Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
@@ -91,6 +91,7 @@ type one_inductive_impls =
   Impargs.manual_implicits list (** for constrs *)
 
 val interp_mutual_inductive :
+  bool -> (* if [false], then positivity is assumed *)
   structured_inductive_expr -> decl_notation list -> polymorphic ->
     private_flag -> Decl_kinds.recursivity_kind ->
     mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
@@ -105,6 +106,7 @@ val declare_mutual_inductive_with_eliminations :
 (** Entry points for the vernacular commands Inductive and CoInductive *)
 
 val do_mutual_inductive :
+  bool -> (* if [false], then positivity is assumed *)
   (one_inductive_expr * decl_notation list) list -> polymorphic -> 
   private_flag -> Decl_kinds.recursivity_kind -> unit
 
@@ -148,12 +150,13 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
+  flags:Declarations.typing_flags ->
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
-val declare_cofixpoint : locality -> polymorphic -> 
+val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -161,14 +164,16 @@ val declare_cofixpoint : locality -> polymorphic ->
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
+  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
+  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+val declare_fix : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
   Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 6b267283a..74361eb1c 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -116,5 +116,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univs
+    mind_entry_universes = univs;
+    mind_entry_check_positivity = mib.mind_checked_positive;
   }
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index f995a390c..a43758e3c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -497,7 +497,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
-  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) then
+  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_checked_positive then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
   if is_eq_flag() then try_declare_beq_scheme kn;
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index dbc3ccaac..00fd97210 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,8 @@ let declare_mutual_definition l =
 	    List.map3 compute_possible_guardness_evidences
               wfl fixdefs fixtypes in
 	  let indexes = 
-            Pretyping.search_guard Loc.ghost (Global.env())
+              Pretyping.search_guard ~tflags:{Declarations.check_guarded=true}
+              Loc.ghost (Global.env())
               possible_indexes fixdecls in
           Some indexes, 
           List.map_i (fun i _ ->
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0c3bd953c..214d44d83 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -361,7 +361,7 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite poly ctx id idbuild paramimpls params arity template 
+let declare_structure chk finite poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Context.Rel.to_extended_list nfields params in
@@ -386,7 +386,8 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_inds = [mie_ind];
       mind_entry_polymorphic = poly;
       mind_entry_private = None;
-      mind_entry_universes = ctx } in
+      mind_entry_universes = ctx;
+      mind_entry_check_positivity = chk; } in
   let kn = Command.declare_mutual_inductive_with_eliminations mie [] [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
@@ -405,7 +406,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map get_name ctx)))
 
-let declare_class finite def poly ctx id idbuild paramimpls params arity 
+let declare_class chk finite def poly ctx id idbuild paramimpls params arity 
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -448,7 +449,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -527,8 +528,9 @@ open Vernacexpr
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
-   or subinstances *)
-let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+   or subinstances. When [chk] is false positivity is
+    assumed. *)
+let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
@@ -549,14 +551,14 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
   let sign = structure_signature (fields@params) in
   let gr = match kind with
     | Class def ->
-	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
+	let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild
 	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite poly ctx idstruc 
+	let ind = declare_structure chk finite poly ctx idstruc 
 	  idbuild implpars params arity template implfs 
 	  fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
 	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 26eb3378b..525326237 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -24,7 +24,9 @@ val declare_projections :
   coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
   (Name.t * bool) list * constant option list
 
-val declare_structure : Decl_kinds.recursivity_kind ->
+val declare_structure :
+  bool -> (** check positivity? *)
+  Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) -> Univ.universe_context ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
@@ -37,6 +39,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   inductive
 
 val definition_structure :
+  bool -> (** check positivity? *)
   inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 222b7d3df..0b4dc0d18 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -519,7 +519,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_record k poly finite struc binders sort nameopt cfs =
+let vernac_record chk k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -530,9 +530,14 @@ let vernac_record k poly finite struc binders sort nameopt cfs =
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
-    ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort))
-
-let vernac_inductive poly lo finite indl =
+    ignore(Record.definition_structure chk (k,poly,finite,struc,binders,cfs,const,sort))
+
+(** When [chk] is false, positivity is assumed. When [poly] is true
+    the type is declared polymorphic. When [lo] is true, then the type
+    is declared private (as per the [Private] keyword). [finite]
+    indicates whether the type is inductive, co-inductive or
+    neither. *)
+let vernac_inductive chk poly lo finite indl =
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -548,14 +553,14 @@ let vernac_inductive poly lo finite indl =
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
       Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
-      vernac_record (match b with Class true -> Class false | _ -> b)
+      vernac_record chk (match b with Class true -> Class false | _ -> b)
        poly finite id bl c oc fs
   | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
 	let coe' = if coe then Some true else None in
   	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
-      in vernac_record (Class true) poly finite id bl c None [f]
+      in vernac_record chk (Class true) poly finite id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
       Errors.error "Definitional classes must have a single method"
   | [ ( id , bl , c , Class false, Constructors _), _ ] ->
@@ -569,19 +574,19 @@ let vernac_inductive poly lo finite indl =
       | _ -> Errors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl poly lo finite
+    do_mutual_inductive chk indl poly lo finite
 
-let vernac_fixpoint locality poly local l =
+let vernac_fixpoint ~flags locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint local poly l
+  do_fixpoint ~flags local poly l
 
-let vernac_cofixpoint locality poly local l =
+let vernac_cofixpoint ~flags locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint local poly l
+  do_cofixpoint ~flags local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1726,6 +1731,7 @@ let vernac_load interp fname =
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()
 
+let all_checks = { Declarations.check_guarded = true }
 
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
@@ -1763,9 +1769,9 @@ let interp ?proof ~loc locality poly c =
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
-  | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l
-  | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
+  | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
+  | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l
+  | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe loc poly l