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.
---
 toplevel/command.ml   | 3 ++-
 toplevel/discharge.ml | 3 ++-
 toplevel/record.ml    | 3 ++-
 3 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1b396d57ba..49bd37c697 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -553,7 +553,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 = Evd.universe_context evd },
+    mind_entry_universes = Evd.universe_context evd;
+    mind_entry_check_positivity = true; },
     impls
 
 (* Very syntactical equality *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 7d5d61fb8b..df4f77fa19 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -115,5 +115,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/record.ml b/toplevel/record.ml
index 737b7fb59f..2f7215adf8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -365,7 +365,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 = true; } 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
-- 
cgit v1.2.3


From 2adff76c5466734c633923e768c9dcbdc6f28c86 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 17:45:04 +0200
Subject: Add corresponding field in `VernacInductive`.

Makes sure not to generate inductive schemes of assumed positive types.
---
 toplevel/command.ml       |  8 ++++----
 toplevel/command.mli      |  2 ++
 toplevel/indschemes.ml    |  2 +-
 toplevel/record.ml        | 21 +++++++++++----------
 toplevel/record.mli       |  5 ++++-
 toplevel/vernacentries.ml | 21 +++++++++++++--------
 6 files changed, 35 insertions(+), 24 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 49bd37c697..ca925d4904 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -475,7 +475,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
@@ -554,7 +554,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
     mind_entry_universes = Evd.universe_context evd;
-    mind_entry_check_positivity = true; },
+    mind_entry_check_positivity = chk; },
     impls
 
 (* Very syntactical equality *)
@@ -636,10 +636,10 @@ 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,impls = interp_mutual_inductive indl ntns poly prv finite in
+  let mie,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 impls);
   (* Declare the possible notations of inductive types *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3a38e52cee..3ec65b487b 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -88,6 +88,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 * one_inductive_impls list
@@ -102,6 +103,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
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index fbc45b4ae3..ca3b0c290c 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -478,7 +478,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/record.ml b/toplevel/record.ml
index 2f7215adf8..259a35c581 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -340,7 +340,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 = Termops.extended_rel_list nfields params in
@@ -366,7 +366,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_polymorphic = poly;
       mind_entry_private = None;
       mind_entry_universes = ctx;
-      mind_entry_check_positivity = true; } in
+      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
@@ -385,7 +385,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map pi1 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. *)
@@ -424,7 +424,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
@@ -500,10 +500,11 @@ let declare_existing_class g =
 
 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)),ps,cfs,idbuild,s) =
+(** [fs] corresponds to fields and [ps] to parameters; [coers] is a
+    list telling if the corresponding fields must me declared as
+    coercions or subinstances. When [chk] is false positivity is
+    assumed. *)
+let definition_structure chk (kind,poly,finite,(is_coe,(loc,idstruc)),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
@@ -524,14 +525,14 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild
   let sign = structure_signature (fields@params) in
     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 91dccb96e1..be04502587 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -25,7 +25,9 @@ val declare_projections :
   coercion_flag list -> manual_explicitation list list -> rel_context ->
   (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 -> rel_context -> (** params *) constr -> (** arity *)
@@ -38,6 +40,7 @@ val declare_structure : Decl_kinds.recursivity_kind ->
   inductive
 
 val definition_structure :
+  bool -> (** check positivity? *)
   inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident 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 8d9f8f52c8..c925719fb7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -521,7 +521,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Pp.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 (snd struc))
     | Some (_,id as lid) ->
@@ -532,9 +532,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
@@ -550,14 +555,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 _), _ ] ->
@@ -571,7 +576,7 @@ 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 local = enforce_locality_exp locality local in
@@ -1889,7 +1894,7 @@ let interp ?proof 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
+  | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
   | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
   | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l
-- 
cgit v1.2.3


From 75381f7356133f68637fc9bbc0a213dcfa6e2c71 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 24 Jun 2015 15:24:49 +0200
Subject: When assuming an inductive type positive, then it is declared
 "unsafe" to the interfaces.

---
 toplevel/command.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ca925d4904..6beaf54c53 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -645,7 +645,10 @@ let do_mutual_inductive chk indl poly prv finite =
   (* 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 Pp.feedback Feedback.AddedAxiom else ()
 
 (* 3c| Fixpoints and co-fixpoints *)
 
-- 
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.

---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6beaf54c53..06d7c629a5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1168,7 +1168,7 @@ let do_program_recursive local p fixkind fixl ntns =
       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
+	List.iteri (fun i _ -> Inductive.check_fix env ~chk:true ((indexes,i),fixdecls)) fixl
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-- 
cgit v1.2.3


From e0547f9e9134a9fff122df900942a094c53535c3 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 26 Jun 2015 21:15:36 +0200
Subject: Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control
 assuming guardedness.

---
 toplevel/command.ml       | 12 ++++++------
 toplevel/command.mli      |  6 +++++-
 toplevel/vernacentries.ml | 12 ++++++------
 3 files changed, 17 insertions(+), 13 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 06d7c629a5..14a1efe4d8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1044,7 +1044,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   fix,Evd.evar_universe_context evd,info
     
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
+let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1080,7 +1080,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
+let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1202,19 +1202,19 @@ 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 ~chkguard 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 fix = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences (pi3 fix) in
-    declare_fixpoint local poly fix possible_indexes ntns
+    declare_fixpoint ~chkguard local poly fix possible_indexes ntns
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~chkguard 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 ~chkguard local poly cofix ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3ec65b487b..7112591fe9 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -146,12 +146,14 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
+  chkguard:bool ->
   locality -> polymorphic ->
   recursive_preentry * 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 :
+  chkguard:bool -> locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -159,9 +161,11 @@ val declare_cofixpoint : locality -> polymorphic ->
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
+  chkguard:bool -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
+  chkguard:bool -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c925719fb7..a0af1d5730 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -578,17 +578,17 @@ let vernac_inductive chk poly lo finite indl =
     let indl = List.map unpack indl in
     do_mutual_inductive chk indl poly lo finite
 
-let vernac_fixpoint locality poly local l =
+let vernac_fixpoint ~chkguard 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 ~chkguard local poly l
 
-let vernac_cofixpoint locality poly local l =
+let vernac_cofixpoint ~chkguard 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 ~chkguard local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1895,8 +1895,8 @@ let interp ?proof locality poly c =
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
   | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
-  | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
+  | VernacFixpoint (chkguard,local, l) -> vernac_fixpoint ~chkguard locality poly local l
+  | VernacCoFixpoint (chkguard,local, l) -> vernac_cofixpoint ~chkguard locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe l
-- 
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.
---
 toplevel/command.ml  | 22 +++++++++++-----------
 toplevel/command.mli |  7 +++++--
 2 files changed, 16 insertions(+), 13 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14a1efe4d8..ac46b439cf 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,9 +139,9 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ident ce local k imps =
+let declare_global_definition ~chkguard ident ce local k imps =
   let local = get_locality ident local in
-  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+  let kn = declare_constant ~chkguard ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = definition_message ident in
@@ -151,7 +151,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 imps hook =
+let declare_definition ~chkguard ident (local, p, k) ce imps hook =
   let () = !declare_definition_hook ce in
   let r = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -167,10 +167,10 @@ let declare_definition ident (local, p, k) ce imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ident ce local k imps in
+    declare_global_definition ~chkguard ident ce local k imps in
   Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
 
-let _ = Obligations.declare_definition_ref := declare_definition
+let _ = Obligations.declare_definition_ref := declare_definition ~chkguard:true
 
 let do_definition ident k bl red_option c ctypopt hook =
   let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
@@ -191,7 +191,7 @@ let do_definition ident k bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ident k ce imps
+      ignore(declare_definition ~chkguard:true ident k ce imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -752,11 +752,11 @@ 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) ctx f ((def,_),eff) t imps =
+let declare_fix ~chkguard ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition ~chkguard f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
-let _ = Obligations.declare_fix_ref := declare_fix
+let _ = Obligations.declare_fix_ref := (declare_fix ~chkguard:true)
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1072,7 +1072,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim
     let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
+    ignore (List.map4 (declare_fix ~chkguard (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1103,7 +1103,7 @@ let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fix
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
     let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx) 
+    ignore (List.map4 (declare_fix ~chkguard (local, poly, CoFixpoint) ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7112591fe9..7578e26c16 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -34,7 +34,8 @@ val interp_definition :
   local_binder list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
-val declare_definition : Id.t -> definition_kind ->
+val declare_definition : chkguard:bool ->
+  Id.t -> definition_kind ->
   definition_entry -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
@@ -172,5 +173,7 @@ val do_cofixpoint :
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix :
+  chkguard:bool ->
+  ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
-- 
cgit v1.2.3


From 0b20282c49253aea4429384467b75a5bdb1f8ba4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Sep 2015 09:39:56 +0200
Subject: Declare assumptions of well-founded definitions as unsafe.

So that fixpoints and cofixpoints which are assumed to be total are highlighted in yellow in Coqide, for instance.
---
 toplevel/command.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ac46b439cf..c6d67b13ac 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1209,7 +1209,8 @@ let do_fixpoint ~chkguard local poly l =
     let fix = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences (pi3 fix) in
-    declare_fixpoint ~chkguard local poly fix possible_indexes ntns
+    declare_fixpoint ~chkguard local poly fix possible_indexes ntns;
+    if not chkguard then Pp.feedback Feedback.AddedAxiom else ()
 
 let do_cofixpoint ~chkguard local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
@@ -1217,4 +1218,5 @@ let do_cofixpoint ~chkguard local poly l =
       do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-	declare_cofixpoint ~chkguard local poly cofix ntns
+      declare_cofixpoint ~chkguard local poly cofix ntns;
+      if not chkguard then Pp.feedback Feedback.AddedAxiom else ()
-- 
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
---
 toplevel/command.ml       | 46 ++++++++++++++++++++++++++--------------------
 toplevel/command.mli      | 12 ++++++------
 toplevel/vernacentries.ml | 12 ++++++------
 3 files changed, 38 insertions(+), 32 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index c6d67b13ac..b6dd2718fa 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,9 +139,9 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ~chkguard ident ce local k imps =
+let declare_global_definition ~flags ident ce local k imps =
   let local = get_locality ident local in
-  let kn = declare_constant ~chkguard 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 () = definition_message ident in
@@ -151,7 +151,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 ~chkguard ident (local, p, k) ce imps hook =
+let declare_definition ~flags ident (local, p, k) ce imps hook =
   let () = !declare_definition_hook ce in
   let r = match local with
   | Discharge when Lib.sections_are_opened () ->
@@ -167,10 +167,11 @@ let declare_definition ~chkguard ident (local, p, k) ce imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ~chkguard ident ce local k imps in
+    declare_global_definition ~flags ident ce local k imps in
   Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
 
-let _ = Obligations.declare_definition_ref := declare_definition ~chkguard:true
+let _ = Obligations.declare_definition_ref :=
+    declare_definition ~flags:{Declarations.check_guarded=true}
 
 let do_definition ident k bl red_option c ctypopt hook =
   let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
@@ -191,7 +192,7 @@ let do_definition ident k bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ~chkguard:true ident k ce imps
+      ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -752,11 +753,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 ~chkguard ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition ~chkguard f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition ~flags f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
-let _ = Obligations.declare_fix_ref := (declare_fix ~chkguard:true)
+let _ = Obligations.declare_fix_ref :=
+    (declare_fix ~flags:{Declarations.check_guarded=true})
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1044,7 +1046,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   fix,Evd.evar_universe_context evd,info
     
-let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
+let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1072,7 +1074,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim
     let ctx = Universes.restrict_universe_context ctx vars in
     let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
     let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix ~chkguard (local, poly, Fixpoint) ctx)
+    ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1080,7 +1082,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
+let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1103,7 +1105,7 @@ let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fix
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
     let ctx = Univ.ContextSet.to_context ctx in
-    ignore (List.map4 (declare_fix ~chkguard (local, poly, CoFixpoint) ctx) 
+    ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1168,7 +1170,11 @@ let do_program_recursive local p fixkind fixl ntns =
       in
       let indexes = 
 	Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in
-	List.iteri (fun i _ -> Inductive.check_fix env ~chk:true ((indexes,i),fixdecls)) fixl
+      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
@@ -1202,21 +1208,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 ~chkguard 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 fix = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences (pi3 fix) in
-    declare_fixpoint ~chkguard local poly fix possible_indexes ntns;
-    if not chkguard then Pp.feedback Feedback.AddedAxiom else ()
+    declare_fixpoint ~flags local poly fix possible_indexes ntns;
+    if not flags.Declarations.check_guarded then Pp.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint ~chkguard 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 ~chkguard local poly cofix ntns;
-      if not chkguard then Pp.feedback Feedback.AddedAxiom else ()
+      declare_cofixpoint ~flags local poly cofix ntns;
+      if not flags.Declarations.check_guarded then Pp.feedback Feedback.AddedAxiom else ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7578e26c16..73f8f98065 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -34,7 +34,7 @@ val interp_definition :
   local_binder list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
-val declare_definition : chkguard:bool ->
+val declare_definition : flags:Declarations.typing_flags ->
   Id.t -> definition_kind ->
   definition_entry -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
@@ -147,14 +147,14 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  chkguard:bool -> locality -> polymorphic ->
+  flags:Declarations.typing_flags -> locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -162,11 +162,11 @@ val declare_cofixpoint :
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  chkguard:bool -> (* When [false], assume guarded. *)
+  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  chkguard:bool -> (* When [false], assume guarded. *)
+  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
@@ -174,6 +174,6 @@ val do_cofixpoint :
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
 val declare_fix :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a0af1d5730..40dfa1b9a5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -578,17 +578,17 @@ let vernac_inductive chk poly lo finite indl =
     let indl = List.map unpack indl in
     do_mutual_inductive chk indl poly lo finite
 
-let vernac_fixpoint ~chkguard 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 ~chkguard local poly l
+  do_fixpoint ~flags local poly l
 
-let vernac_cofixpoint ~chkguard 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 ~chkguard local poly l
+  do_cofixpoint ~flags local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1895,8 +1895,8 @@ let interp ?proof locality poly c =
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
   | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
-  | VernacFixpoint (chkguard,local, l) -> vernac_fixpoint ~chkguard locality poly local l
-  | VernacCoFixpoint (chkguard,local, l) -> vernac_cofixpoint ~chkguard locality poly local l
+  | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l
+  | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe l
-- 
cgit v1.2.3


From 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 15 Jun 2016 19:19:58 +0200
Subject: Allow `Pretyping.search_guard` to not check guard

This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.

Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
---
 toplevel/command.ml     | 6 ++++--
 toplevel/obligations.ml | 3 ++-
 2 files changed, 6 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index b6dd2718fa..c4f0b7b17f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1065,7 +1065,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps)
     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 =
@@ -1169,7 +1169,9 @@ 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
+        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}
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9df5a411ba..ec58392d51 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -582,7 +582,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 _ ->
-- 
cgit v1.2.3


From dcf4d3e28813e09fc71f974b79ddf42d2e525976 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 5 Jun 2016 21:50:22 +0200
Subject: Remove the syntax changes introduced by this branch.

We decided to only export the API, so that an external plugin can provide
this feature without having to merge it in current Coq trunk. This postpones
the attribute implementation in vernacular commands after 8.6.
---
 toplevel/vernacentries.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 40dfa1b9a5..a5e771d75d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1856,6 +1856,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
@@ -1894,9 +1895,9 @@ let interp ?proof 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 (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
-  | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l
-  | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags 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 l
-- 
cgit v1.2.3