Add corresponding field in `VernacInductive`.

Makes sure not to generate inductive schemes of assumed positive types.

13 files changed, 46 insertions, 33 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d7b269a1de..5fff21e270 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -303,7 +303,9 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * simple_binder with_coercion list
-  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of
+      bool (*[false] => assume positive*) *
+      private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e8a1b512c0..be11b86adb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -204,7 +204,7 @@ GEXTEND Gram
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (priv,f,indl)
+          VernacInductive (true,priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 065c12a2d7..b4febba668 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1424,7 +1424,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
+    with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1435,7 +1435,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1450,7 +1450,7 @@ let do_build_inductive
 	in
 	let msg =
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    Errors.print reraise
 	in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index ea699580b9..8c4bd484f5 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -884,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,impls = Command.interp_mutual_inductive indl [] 
+  let mie,impls = Command.interp_mutual_inductive true indl [] 
           false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (Command.declare_mutual_inductive_with_eliminations mie impls)
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 832c08fe0e..a65bfd44d7 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -761,7 +761,7 @@ module Make
               (pr_assumption_token (n > 1) stre ++ spc() ++
                  pr_ne_params_list pr_lconstr_expr l)
           )
-        | VernacInductive (p,f,l) ->
+        | VernacInductive (chk,p,f,l) ->
           let pr_constructor (coe,(id,c)) =
             hov 2 (pr_lident id ++ str" " ++
                      (if coe then str":>" else str":") ++
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 9edc1f1c70..4cc362ddab 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -580,7 +580,7 @@ let rec tmpp v loc =
       let l = match l with Some x -> x | None -> Decl_kinds.Global in
       let kind = string_of_assumption_kind l a many in
       xmlAssumption kind loc exprs
-  | VernacInductive (_, _, iednll) ->
+  | VernacInductive (_,_, _, iednll) ->
       let kind =
         let (_, _, _, k, _),_ = List.hd iednll in
 	  begin
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2b5eb86834..03ade646b2 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -144,7 +144,7 @@ let rec classify_vernac e =
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
         VtSideff ids, VtLater    
     | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
-    | VernacInductive (_,_,l) ->
+    | VernacInductive (_,_,_,l) ->
         let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
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