From 04f278b3b3d0832413fd1853bcb6558a4c305397 Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Mon, 5 Nov 2018 11:18:08 +0100
Subject: [PATCH 1/8] Split the [check_guarded] typing_flag into
 [check_guarded] (for (co)fixpoints) and [check_positive] (for (co)inductive
 types).

---
 checker/values.ml      | 2 +-
 kernel/declarations.ml | 2 ++
 kernel/declareops.ml   | 1 +
 kernel/indtypes.ml     | 2 +-
 vernac/assumptions.ml  | 2 +-
 vernac/comInductive.ml | 2 +-
 vernac/indschemes.ml   | 2 +-
 7 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/checker/values.ml b/checker/values.ml
index e21acd817993..4c5f7e6ebb58 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -229,7 +229,7 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_typing_flags =
-  v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
+  v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
 
 let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c1b38b4156ab..90695e6445dd 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -63,6 +63,8 @@ type constant_universes =
 type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
+  check_positive : bool; (** If [false] then inductive types are assumed positive
+                               and co-inductive types are assumed productive. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
   conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
   share_reduction : bool; (** Use by-need reduction algorithm *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c5387a..b77c5a1295e9 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,6 +19,7 @@ module RelDecl = Context.Rel.Declaration
 
 let safe_flags oracle = {
   check_guarded = true;
+  check_positive = true;
   check_universes = true;
   conv_oracle = oracle;
   share_reduction = true;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 20c90bc05a1b..5e89cb8dc97f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -973,7 +973,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let chkpos = (Environ.typing_flags env).check_guarded in
+  let chkpos = (Environ.typing_flags env).check_positive in
   let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_private mie.mind_entry_universes
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 6beac2032dda..5d74c6ed253f 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -326,7 +326,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
       let mind = lookup_mind m in
-      if mind.mind_typing_flags.check_guarded then
+      if mind.mind_typing_flags.check_positive then
         accu
       else
         let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f405c4d5a934..947ee91ea82c 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -572,4 +572,4 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite =
   (* Declare the coercions *)
   List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
-  if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  if not (typing_flags (Global.env ())).Declarations.check_positive then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c1343fb59296..47163223e466 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -542,7 +542,7 @@ 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 <> Declarations.BiFinite || !bifinite_elim_flag)
-     && mib.mind_typing_flags.check_guarded then
+     && mib.mind_typing_flags.check_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;

From ef45cf813f4ea8eb51c323e6fa2bebbb58e667e7 Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Mon, 5 Nov 2018 11:45:47 +0100
Subject: [PATCH 2/8] Add [Print Typing Flags] command.

---
 printing/printer.ml     | 5 +++++
 printing/printer.mli    | 1 +
 vernac/g_vernac.mlg     | 1 +
 vernac/ppvernac.ml      | 2 ++
 vernac/vernacentries.ml | 1 +
 vernac/vernacexpr.ml    | 1 +
 6 files changed, 11 insertions(+)

diff --git a/printing/printer.ml b/printing/printer.ml
index da364c8b9e0a..aaab13952c83 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -995,3 +995,8 @@ let print_and_diff oldp newp =
         pr_open_subgoals ~proof
     in
     Feedback.msg_notice output;;
+
+let pr_typing_flags flags =
+  str "check_guarded: " ++ bool flags.check_guarded ++ fnl ()
+  ++ str "check_positive: " ++ bool flags.check_positive ++ fnl ()
+  ++ str "check_universes: " ++ bool flags.check_universes
diff --git a/printing/printer.mli b/printing/printer.mli
index f9d1a6289573..1fc24e4c8ee6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -208,3 +208,4 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 
+val pr_typing_flags : Declarations.typing_flags -> Pp.t
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 1d0a5ab0a3be..b4689a9f12f4 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -979,6 +979,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Coercion"; IDENT "Paths"; s = class_rawexpr; t = class_rawexpr
          -> { PrintCoercionPaths (s,t) }
       | IDENT "Canonical"; IDENT "Projections" -> { PrintCanonicalConversions }
+      | IDENT "Typing"; IDENT "Flags" -> { PrintTypingFlags }
       | IDENT "Tables" -> { PrintTables }
       | IDENT "Options" -> { PrintTables (* A Synonymous to Tables *) }
       | IDENT "Hint" -> { PrintHintGoal }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1c1faca5992a..c889f0e92112 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -482,6 +482,8 @@ open Pputils
       ++ pr_class_rawexpr t
     | PrintCanonicalConversions ->
       keyword "Print Canonical Structures"
+    | PrintTypingFlags ->
+      keyword "Print Typing Flags"
     | PrintTables ->
       keyword "Print Tables"
     | PrintHintGoal ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1fab35b650d3..df7c75338247 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1802,6 +1802,7 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
 
 let vernac_print ~atts env sigma =
   function
+  | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ()))
   | PrintTables -> print_tables ()
   | PrintFullContext-> print_full_context_typ env sigma
   | PrintSectionContext qid -> print_sec_context_typ env sigma qid
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 594e9eca4849..c1366b1e9e3c 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -24,6 +24,7 @@ type goal_reference =
   | GoalId of Id.t
 
 type printable =
+  | PrintTypingFlags
   | PrintTables
   | PrintFullContext
   | PrintSectionContext of qualid

From 8a7d8d2c1e94e2a9512512d1eb8e3fcf0c0669b3 Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Thu, 15 Nov 2018 09:14:18 +0100
Subject: [PATCH 3/8] Add guarded/positivity/universes attributes.

---
 kernel/environ.ml       |  7 +++++++
 kernel/environ.mli      |  3 +++
 library/global.ml       | 10 ++++++++++
 library/global.mli      |  5 +++++
 printing/printer.ml     |  4 ++--
 vernac/attributes.ml    | 13 +++++++++++++
 vernac/attributes.mli   |  6 ++++++
 vernac/comFixpoint.ml   | 38 +++++++++++++++++++++++++-------------
 vernac/comFixpoint.mli  | 11 +++++------
 vernac/lemmas.ml        |  2 ++
 vernac/lemmas.mli       |  3 +++
 vernac/vernacentries.ml | 38 +++++++++++++++++++++++++++++---------
 12 files changed, 110 insertions(+), 30 deletions(-)

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f61dd0c10107..beca846f93c3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -233,6 +233,13 @@ let set_oracle env o =
 let engagement env = env.env_stratification.env_engagement
 let typing_flags env = env.env_typing_flags
 
+let update_check_guarded flags opt =
+  Option.cata (fun b -> {flags with check_guarded = b}) flags opt
+let update_check_positive flags opt =
+  Option.cata (fun b -> {flags with check_positive = b}) flags opt
+let update_check_universes flags opt =
+  Option.cata (fun b -> {flags with check_universes = b}) flags opt
+
 let is_impredicative_set env = 
   match engagement env with
   | ImpredicativeSet -> true
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c285f907fcd3..ceb67a4dcdc6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -93,6 +93,9 @@ val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 val engagement    : env -> engagement
 val typing_flags    : env -> typing_flags
+val update_check_guarded : typing_flags -> bool option -> typing_flags
+val update_check_positive : typing_flags -> bool option -> typing_flags
+val update_check_universes : typing_flags -> bool option -> typing_flags
 val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
diff --git a/library/global.ml b/library/global.ml
index 4ea5969a6fb2..1f5bdbc9c6aa 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -90,6 +90,16 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
 let typing_flags () = Environ.typing_flags (env ())
+let update_check_guarded = function
+  | Some b -> set_typing_flags {(typing_flags ()) with Declarations.check_guarded = b}
+  | None -> ()
+let update_check_positive = function
+  | Some b -> set_typing_flags {(typing_flags ()) with Declarations.check_positive = b}
+  | None -> ()
+let update_check_universes = function
+  | Some b -> set_typing_flags {(typing_flags ()) with Declarations.check_universes = b}
+  | None -> ()
+
 let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd)
 let add_constant ~in_section id d = globalize (Safe_typing.add_constant ~in_section (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
diff --git a/library/global.mli b/library/global.mli
index 01ee695c49b2..651183c5cda5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,6 +32,11 @@ val set_engagement : Declarations.engagement -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
 val typing_flags : unit -> Declarations.typing_flags
 
+(** Changing some typing flags (does nothing if None) *)
+val update_check_guarded : bool option -> unit
+val update_check_positive : bool option -> unit
+val update_check_universes : bool option -> unit
+
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
diff --git a/printing/printer.ml b/printing/printer.ml
index aaab13952c83..6449d03a43ff 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -911,9 +911,9 @@ let pr_assumptionset env sigma s =
       | Constant kn ->
           safe_pr_constant env kn ++ safe_pr_ltype env sigma typ
       | Positive m ->
-          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded kn ->
-          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.")
+          hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is assumed to be guarded.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 88638b295b0d..1a62818f9dc5 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -73,6 +73,9 @@ let mk_deprecation ?(since=None) ?(note=None) () =
 
 type t = {
   locality : bool option;
+  (* check_guard : bool option; *)
+  (* check_positivity : bool option; *)
+  (* check_universes : bool option; *)
   polymorphic : bool;
   template : bool option;
   program : bool;
@@ -134,6 +137,12 @@ let program = program_opt >>= function
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
+let check_guard = bool_attribute ~name:"Check Guard" ~on:"check_guarded" ~off:"assume_guarded"
+
+let check_positivity = bool_attribute ~name:"Check Positivity" ~on:"check_positive" ~off:"assume_positive"
+
+let check_universes = bool_attribute ~name:"Check Universes" ~on:"check_universes" ~off:"type_in_type"
+
 let warn_unqualified_univ_attr =
   CWarnings.create ~name:"unqualified-univ-attr" ~category:"deprecated"
     (fun key -> Pp.(str "Attribute " ++ str key ++
@@ -205,6 +214,10 @@ let attributes_of_flags f =
     parse (locality ++ deprecation ++ universe_poly_template ++ program) f
   in
   { polymorphic; program; locality; template; deprecated }
+  (* let (((((locality, check_guard), check_positivity), check_universes), deprecated), (polymorphic, template)), program = *)
+  (*   parse (locality ++ check_guard ++ check_positivity ++ check_universes ++ deprecation ++ universe_poly_template ++ program) f *)
+  (* in *)
+  (* { locality; check_guard; check_positivity; check_universes; deprecated; polymorphic; template; program } *)
 
 let only_locality atts = parse locality atts
 
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index c81082d5addc..e8e454e2e131 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -45,6 +45,9 @@ val polymorphic : bool attribute
 val program : bool attribute
 val universe_poly_template : (bool * bool option) attribute
 val locality : bool option attribute
+val check_guard : bool option attribute
+val check_positivity : bool option attribute
+val check_universes : bool option attribute
 val deprecation : deprecation option attribute
 
 val program_opt : bool option attribute
@@ -52,6 +55,9 @@ val program_opt : bool option attribute
 
 type t = {
   locality : bool option;
+  (* check_guard : bool option; (\* None -> use global env typing flags ; Some -> override *\) *)
+  (* check_positivity : bool option; (\* None -> use global env typing flags ; Some -> override *\) *)
+  (* check_universes : bool option; (\* None -> use global env typing flags ; Some -> override *\) *)
   polymorphic : bool;
   template : bool option;
   program : bool;
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a9c499b1920f..30b7b1b50462 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -250,7 +250,7 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint original_typing_flag 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 =
@@ -261,7 +261,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
         fixdefs) in
     let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint)
-      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> Global.set_typing_flags original_typing_flag))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -280,12 +280,13 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
               fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
+    Global.set_typing_flags original_typing_flag;
     fixpoint_message (Some indexes) fixnames;
   end;
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
 
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint original_typing_flag 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 =
@@ -296,7 +297,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
         fixdefs) in
     let evd = Evd.from_ctx ctx in
       Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
-      evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
+      evd pl (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> Global.set_typing_flags original_typing_flag))
   else begin
     (* We shortcut the proof process *)
     let fixdefs = List.map Option.get fixdefs in
@@ -312,6 +313,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
               fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
+    Global.set_typing_flags original_typing_flag;
     cofixpoint_message fixnames
   end;
   (* Declare notations *)
@@ -338,21 +340,31 @@ let extract_cofixpoint_components l =
              fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
-let check_safe () =
+let check_safe check_guard check_universes =
   let open Declarations in
   let flags = Environ.typing_flags (Global.env ()) in
-  flags.check_universes && flags.check_guarded
+  (Option.default flags.check_guarded check_guard)
+  && (Option.default flags.check_universes check_universes)
 
-let do_fixpoint local poly l =
+
+let do_fixpoint ?check_guard ?check_universes local poly l =
+  let original_typing_flag = Environ.typing_flags (Global.env ()) in
+  Global.update_check_guarded check_guard;
+  Global.update_check_universes check_universes;
   let fixl, ntns = extract_fixpoint_components true l in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
   let possible_indexes =
     List.map compute_possible_guardness_evidences info in
-  declare_fixpoint local poly fix possible_indexes ntns;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
-
-let do_cofixpoint local poly l =
+  (* We delegate to declare_fixpoint the role to set the original typing flag so that it can be in a hook if needed *)
+  declare_fixpoint original_typing_flag local poly fix possible_indexes ntns;
+  if not (check_safe check_guard check_universes) then Feedback.feedback Feedback.AddedAxiom else ()
+
+let do_cofixpoint ?check_guard ?check_universes local poly l =
+  let original_typing_flag = Environ.typing_flags (Global.env ()) in
+  Global.update_check_guarded check_guard;
+  Global.update_check_universes check_universes;
   let fixl,ntns = extract_cofixpoint_components l in
   let cofix = interp_fixpoint ~cofix:true fixl ntns in
-  declare_cofixpoint local poly cofix ntns;
-  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+  (* We delegate to declare_cofixpoint the role to set the original typing flag *)
+  declare_cofixpoint original_typing_flag local poly cofix ntns;
+  if not (check_safe check_guard check_universes) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index f4569ed3e2fc..42420150a761 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,12 +19,10 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+  ?check_guard:bool -> ?check_universes:bool -> locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  (* When [false], assume guarded. *)
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+  ?check_guard:bool -> ?check_universes:bool -> locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (************************************************************************)
 (** Internal API  *)
@@ -80,12 +78,13 @@ val interp_fixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 (** [Not used so far] *)
 val declare_fixpoint :
-  locality -> polymorphic ->
+  Declarations.typing_flags -> locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
-val declare_cofixpoint : locality -> polymorphic ->
+val declare_cofixpoint :
+  Declarations.typing_flags -> locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3b041b7065d7..74dfd3a22b62 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -36,6 +36,8 @@ module NamedDecl = Context.Named.Declaration
 
 type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
 let mk_hook hook = hook
+let compose_hook h1 h2 =
+  fun l r -> h1 l r; h2 l r
 let call_hook fix_exn hook l c =
   try hook l c
   with e when CErrors.noncritical e ->
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 195fcbf4cac9..859bce477fdd 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -13,6 +13,9 @@ open Decl_kinds
 
 type declaration_hook
 val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
+
+(** [compose_hook h1 h2] is [h1; h2]*)
+val compose_hook : declaration_hook -> declaration_hook -> declaration_hook
 val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> GlobRef.t -> unit
 
 val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index df7c75338247..903c40788d4a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -480,7 +480,12 @@ let vernac_definition_hook p = function
 | _ -> no_hook
 
 let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
+  let atts, check_guard = parse_with_extra check_guard atts in
+  let atts, check_universes = parse_with_extra check_universes atts in
   let atts = attributes_of_flags atts in
+  let original_typing_flag = Environ.typing_flags (Global.env ()) in
+  Global.update_check_guarded check_guard;
+  Global.update_check_universes check_universes;
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let () =
@@ -499,8 +504,9 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
-      start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
-        [(CAst.make ?loc name, pl), (bl, t)] hook
+       let hook' = Lemmas.mk_hook (fun _ _ -> Global.set_typing_flags original_typing_flag) in
+       start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
+        [(CAst.make ?loc name, pl), (bl, t)]  (Lemmas.compose_hook hook hook')
     | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
           | None -> None
@@ -508,7 +514,8 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
             let sigma, env = Pfedit.get_current_context () in
             Some (snd (Hook.get f_interp_redexp env sigma r)) in
       ComDefinition.do_definition ~program_mode name
-        (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
+        (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook;
+      Global.set_typing_flags original_typing_flag)
 
 let vernac_start_proof ~atts kind l =
   let atts = attributes_of_flags atts in
@@ -599,7 +606,12 @@ let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive ~atts cum lo finite indl =
+  let atts, check_positivity = parse_with_extra check_positivity atts in
+  let atts, check_universes = parse_with_extra check_universes atts in
   let atts = attributes_of_flags atts in
+  let original_typing_flag = Environ.typing_flags (Global.env ()) in
+  Global.update_check_positive check_positivity;
+  Global.update_check_universes check_universes;
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -631,7 +643,8 @@ let vernac_inductive ~atts cum lo finite indl =
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
     let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
-    vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+    vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]];
+    Global.set_typing_flags original_typing_flag
   else if List.for_all is_record indl then
     (** Mutual record case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -654,7 +667,8 @@ let vernac_inductive ~atts cum lo finite indl =
     let ((_, _, _, kind, _), _) = List.hd indl in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record ~template udecl cum kind atts.polymorphic finite recordl
+    vernac_record ~template udecl cum kind atts.polymorphic finite recordl;
+    Global.set_typing_flags original_typing_flag
   else if List.for_all is_constructor indl then
     (** Mutual inductive case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -680,9 +694,11 @@ let vernac_inductive ~atts cum lo finite indl =
     let indl = List.map unpack indl in
     let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite;
+    Global.set_typing_flags original_typing_flag
   else
-    user_err (str "Mixed record-inductive definitions are not allowed")
+    (Global.set_typing_flags original_typing_flag;
+     user_err (str "Mixed record-inductive definitions are not allowed"))
 (*
 
   match indl with
@@ -695,6 +711,8 @@ let vernac_inductive ~atts cum lo finite indl =
     *)
 
 let vernac_fixpoint ~atts discharge l =
+  let atts, check_guard = parse_with_extra check_guard atts in
+  let atts, check_universes = parse_with_extra check_universes atts in
   let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
@@ -703,11 +721,13 @@ let vernac_fixpoint ~atts discharge l =
   let do_fixpoint = if Flags.is_program_mode () then
       ComProgramFixpoint.do_fixpoint
     else
-      ComFixpoint.do_fixpoint
+      ComFixpoint.do_fixpoint ?check_guard ?check_universes
   in
   do_fixpoint local atts.polymorphic l
 
 let vernac_cofixpoint ~atts discharge l =
+  let atts, check_guard = parse_with_extra check_guard atts in
+  let atts, check_universes = parse_with_extra check_universes atts in
   let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
@@ -715,7 +735,7 @@ let vernac_cofixpoint ~atts discharge l =
   let do_cofixpoint = if Flags.is_program_mode () then
       ComProgramFixpoint.do_cofixpoint
     else
-      ComFixpoint.do_cofixpoint
+      ComFixpoint.do_cofixpoint ?check_guard ?check_universes
   in
   do_cofixpoint local atts.polymorphic l
 

From 5000fb1948f48fbfe4b0d28314fda80c025c451e Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Wed, 14 Nov 2018 16:07:38 +0100
Subject: [PATCH 4/8] Set/Unset commands for typing flags

---
 vernac/vernacentries.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 903c40788d4a..3c7cb854182e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1625,6 +1625,30 @@ let _ =
       optread  = Nativenorm.get_profiling_enabled;
       optwrite = Nativenorm.set_profiling_enabled }
 
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "guard checking";
+      optkey   = ["Guard"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
+      optwrite = (fun b -> Global.update_check_guarded (Some b)) }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "positivity/productivity checking";
+      optkey   = ["Positivity"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
+      optwrite = (fun b -> Global.update_check_positive (Some b)) }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "universes checking";
+      optkey   = ["Universes"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
+      optwrite = (fun b -> Global.update_check_universes (Some b)) }
+
 let vernac_set_strategy ~local l =
   let local = Option.default false local in
   let glob_ref r =

From 79c76eaf754a28e466fa5dd23b59042c6157ccae Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Thu, 15 Nov 2018 09:36:04 +0100
Subject: [PATCH 5/8] Fix Print Assumptions for Type In Type.

---
 printing/printer.ml   | 3 +++
 printing/printer.mli  | 1 +
 vernac/assumptions.ml | 8 +++++++-
 3 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/printing/printer.ml b/printing/printer.ml
index 6449d03a43ff..ed0bfe38fea9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -838,6 +838,7 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of Constant.t (* a which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
@@ -914,6 +915,8 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded kn ->
           hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TypeInType kn ->
+         hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
     let fold t typ accu =
       let (v, a, o, tr) = accu in
diff --git a/printing/printer.mli b/printing/printer.mli
index 1fc24e4c8ee6..1a833b4c27d6 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -193,6 +193,7 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of Constant.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TypeInType of Constant.t (* a which relies on type in type *)
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 5d74c6ed253f..92f624520f64 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -312,7 +312,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_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) || not cb.const_typing_flags.check_universes then
+      let accu =
+        if cb.const_typing_flags.check_universes then accu
+        else
+          let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+          ContextObjectMap.add (Axiom (TypeInType kn, l)) Constr.mkProp accu
+      in
+    if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
       let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
       ContextObjectMap.add (Axiom (Constant kn,l)) t accu

From 7977e0fcdf3ad947ab34e609a7f80eb6d57a33d2 Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Thu, 15 Nov 2018 09:42:08 +0100
Subject: [PATCH 6/8] Add a file for typing_flags in the test-suite.

---
 test-suite/success/typing_flags.v | 79 +++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)
 create mode 100644 test-suite/success/typing_flags.v

diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
new file mode 100644
index 000000000000..7e1a65bbd006
--- /dev/null
+++ b/test-suite/success/typing_flags.v
@@ -0,0 +1,79 @@
+
+(* Print Typing Flags. *)
+#[type_in_type, assume_guarded] Fixpoint f' (n : nat) : nat := f' n.
+
+#[assume_guarded, local] Fixpoint f (n : nat) : nat.
+Proof.
+  exact (f n).
+(* Print Typing Flags. *)
+Defined.
+
+(* Print Typing Flags. *)
+
+Unset Universes Checking.
+
+(* Print Tables. *)
+(* Test Universes Checking. *)
+
+Definition T := Type.
+Fixpoint g (n : nat) : T := T.
+
+(* Print Typing Flags. *)
+Set Universes Checking.
+
+#[type_in_type] Fixpoint g1 (n : nat) : T.
+Proof.
+  (* Print Typing Flags. *)
+  exact T.
+Defined.
+Set Universes Checking.
+
+Fail Definition g2 (n : nat) : T := T.
+#[type_in_type] Definition g2 (n : nat) : T := T.
+(* Print Typing Flags. *)
+
+Unset Guard Checking.
+Fail #[check_guarded] Definition e := fix e (n : nat) : nat := e n.
+Definition e := fix e (n : nat) : nat := e n.
+Set Guard Checking.
+
+Unset Positivity Checking.
+Inductive Cor :=
+| Over : Cor
+| Next : ((Cor -> list nat) -> list nat) -> Cor.
+Set Positivity Checking.
+(* Print Typing Flags. *)
+(* Print Assumptions Cor. *)
+
+
+
+#[check_universes, assume_guarded] Definition e2 : nat -> nat.
+Proof.
+  exact (fix e (n : nat) : nat := e n).
+Defined.
+(* Print Typing Flags. *)
+Section b.
+  Unset Universes Checking.
+  Variable T : let t := Type in (t : t).
+  Definition T' := T.
+  (* Print Assumptions T'. *)
+  (* Print Typing Flags. *)
+End b.
+(* Print Typing Flags. *)
+Set Universes Checking.
+(* Print Assumptions T'. *)
+
+(* Unset Universes Checking. *)
+#[type_in_type] Inductive T4  := a : let t := Type in (t : t) -> T4.
+Module b.
+  Unset Guard Checking.
+  Global Unset Universes Checking.
+  (* Disable Type In Type. *)
+  Definition T := let t := Type in (t : t).
+  (* Print Typing Flags. *)
+End b.
+(* Print Typing Flags. *)
+Import b.
+(* Print Typing Flags. *)
+(* About T. *)
+(* Print Assumptions T. *)

From 55a987dae171bd69bcefc47a9c54458f73b5b83d Mon Sep 17 00:00:00 2001
From: SimonBoulier <simon.boulier@ens-rennes.fr>
Date: Thu, 15 Nov 2018 12:12:58 +0100
Subject: [PATCH 7/8] Add documentation for typing flags.

---
 CHANGES.md                                    |  3 +
 .../gallina-specification-language.rst        | 29 ++++++++-
 .../proof-engine/vernacular-commands.rst      | 60 +++++++++++++++++++
 test-suite/success/typing_flags.v             |  3 +
 4 files changed, 93 insertions(+), 2 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index c830bc7a1c1b..cf203dcf9b83 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -55,6 +55,9 @@ Vernacular commands
 - Binders for an `Instance` now act more like binders for a `Theorem`.
   Names may not be repeated, and may not overlap with section variable names.
 
+- New commands and attributes to enable/disable guard checking, positivity checking
+  and universes checking (providing a local `-type-in-type`).
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 1a33a9a46ea8..cf31ca07124f 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -776,7 +776,9 @@ Simple inductive types
 
       The types of the constructors have to satisfy a *positivity condition*
       (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition.
+      the inductive definition. The positivity checking can be disable using
+      the command :cmd:`Unset Positivity Checking` or the attribute
+      ``assume_positive`` (see :ref:`gallina-attributes`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
@@ -1500,7 +1502,7 @@ the following attributes names are recognized:
     (see :ref:`programs`).
 
 ``global``, ``local``
-    Take no value, analogous to the ``Global`` and ``Local`` flags
+    Takes no value, analogous to the ``Global`` and ``Local`` flags
     (see :ref:`controlling-locality-of-commands`).
 
 ``deprecated``
@@ -1533,6 +1535,29 @@ the following attributes names are recognized:
           now foo.
         Abort.
 
+``check_guarded``, ``assume_guarded``
+    Takes no value. Enable/disable the guard checking of fixpoints during a
+    definition (see also :ref:`controlling-typing-flags`). Works with
+    :cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`CoFixpoint`, :cmd:`Theorem`
+    (and its variants).
+
+``check_positive``, ``assume_positive``
+    Takes no value. Enable/disable the positivity checking for the declaration
+    of an inductive type or the productivity checking for a coinductive type
+    (see also :ref:`controlling-typing-flags`).
+
+``check_universes``, ``type_in_type``
+    Takes no value. Enable/disable the checking of universes during a definition
+    or the declaration of a (co)inductive type.
+    (see also :ref:`controlling-typing-flags`).
+
+.. example::
+
+   .. coqtop:: all reset
+
+        #[assume_guarded] Fixpoint f (n : nat) : False
+          := f n.
+
 .. [1]
    This is similar to the expression “*entry* :math:`\{` sep *entry*
    :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a69cf209c749..781da6e0cdfe 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1202,6 +1202,66 @@ scope of their effect. There are four kinds of commands:
   occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
   category.
 
+
+.. _controlling-typing-flags:
+
+Controlling Typing Flags
+----------------------------
+
+.. cmd:: Set Guard Checking
+.. cmd:: Unset Guard Checking
+
+   Enable/Disable the guard checking of fixpoints. Warning: this can break the
+   consistency of the system, use at your own risk. Decreasing argument can
+   still be specified but the decrease is not checked anymore. Unchecked
+   fixpoint are printed by :cmd:`Print Assumptions`.
+
+.. cmd:: Set Positivity Checking
+.. cmd:: Unset Positivity Checking
+
+   Enable/Disable the positivity checking of inductive types and the productivity
+   checking of coinductive types. Warning: this can break the consistency of the
+   system, use at your own risk. Unchecked (co)inductive types are printed by
+   :cmd:`Print Assumptions`.
+
+.. cmd:: Set Universes Checking
+.. cmd:: Unset Universes Checking
+
+   Enable/Disable the checking of universes, providing a form of "type in type".
+   Warning: this breaks the consistency of the system, use at your own risk.
+   Constants relying on "type in type" are printed by :cmd:`Print Assumptions`.
+
+.. cmd:: Print Typing Flags
+
+   Print the status of the three typing flags: check of guard, check of positivity
+   and check of universes.
+
+.. example::
+
+   .. coqtop:: all reset
+
+        Unset Guard Checking.
+
+        Print Typing Flags.
+
+        Fixpoint f (n : nat) : False
+          := f n.
+
+        Fixpoint ackermann (m n : nat) {struct m} : nat :=
+          match m with
+          | 0 => S n
+          | S m =>
+            match n with
+            | 0 => ackermann m 1
+            | S n => ackermann m (ackermann (S m) n)
+            end
+          end.
+
+        Print Assumptions ackermann.
+
+   Note that the proper way to define the Ackermann function is to use
+   well-founded recursion (see :cmd:`Program Fixpoint`).
+
 .. _exposing-constants-to-ocaml-libraries:
 
 Exposing constants to OCaml libraries
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index 7e1a65bbd006..7f937fbfa84b 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -37,6 +37,9 @@ Fail #[check_guarded] Definition e := fix e (n : nat) : nat := e n.
 Definition e := fix e (n : nat) : nat := e n.
 Set Guard Checking.
 
+#[assumed_positive] Inductive T :=
+y : (T -> T) -> T.
+
 Unset Positivity Checking.
 Inductive Cor :=
 | Over : Cor

From 738eb146ebc7392d4d8a5594da7c0aec2acdd028 Mon Sep 17 00:00:00 2001
From: SimonBoulier <SimonBoulier@users.noreply.github.com>
Date: Mon, 3 Jun 2019 12:56:40 +0200
Subject: [PATCH 8/8] Update
 doc/sphinx/language/gallina-specification-language.rst
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
---
 doc/sphinx/language/gallina-specification-language.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index cf31ca07124f..6d03452d3133 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -776,7 +776,7 @@ Simple inductive types
 
       The types of the constructors have to satisfy a *positivity condition*
       (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition. The positivity checking can be disable using
+      the inductive definition. The positivity checking can be disabled using
       the command :cmd:`Unset Positivity Checking` or the attribute
       ``assume_positive`` (see :ref:`gallina-attributes`).