Fix bugs and add an option for cumulativity

6 files changed, 42 insertions, 24 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index 6c5997623..2345cb4c5 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -573,7 +573,7 @@ let check_param = function
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
 
-let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
+let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   let env0 = Global.env() in
@@ -657,6 +657,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       mind_entry_finite = finite;
       mind_entry_inds = entries;
       mind_entry_polymorphic = poly;
+      mind_entry_cumulative = cum;
       mind_entry_private = if prv then Some false else None;
       mind_entry_universes = ground_uinfind;
     }
@@ -747,10 +748,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 indl cum poly prv finite =
   let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive indl ntns cum poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
diff --git a/vernac/command.mli b/vernac/command.mli
index 2a52d9bcb..a636bc03c 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -90,9 +90,9 @@ type one_inductive_impls =
   Impargs.manual_implicits list (** for constrs *)
 
 val interp_mutual_inductive :
-  structured_inductive_expr -> decl_notation list -> polymorphic ->
-    private_flag -> Decl_kinds.recursivity_kind ->
-    mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
+  structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+  polymorphic -> private_flag -> Decl_kinds.recursivity_kind ->
+  mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
 
 (** Registering a mutual inductive definition together with its
    associated schemes *)
@@ -104,8 +104,8 @@ val declare_mutual_inductive_with_eliminations :
 (** Entry points for the vernacular commands Inductive and CoInductive *)
 
 val do_mutual_inductive :
-  (one_inductive_expr * decl_notation list) list -> polymorphic -> 
-  private_flag -> Decl_kinds.recursivity_kind -> unit
+  (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+  polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit
 
 (** {6 Fixpoints and cofixpoints} *)
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index c7a741c13..738e27f63 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -116,6 +116,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_params = params';
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
+    mind_entry_cumulative = mib.mind_cumulative;
     mind_entry_private = mib.mind_private;
     mind_entry_universes = univ_info_ind
   }
diff --git a/vernac/record.ml b/vernac/record.ml
index 093a31c19..8a83dceef 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -377,7 +377,7 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite poly ctx id idbuild paramimpls params arity template 
+let declare_structure finite cum poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
   let args = Context.Rel.to_extended_list mkRel nfields params in
@@ -401,6 +401,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_finite = finite;
       mind_entry_inds = [mie_ind];
       mind_entry_polymorphic = poly;
+      mind_entry_cumulative = cum;
       mind_entry_private = None;
       mind_entry_universes = ctx;
     }
@@ -435,7 +436,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class finite def poly ctx id idbuild paramimpls params arity 
+let declare_class finite def cum 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. *)
@@ -478,7 +479,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 (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite cum poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -552,7 +553,7 @@ open Vernacexpr
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions 
    or subinstances. *)
-let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
+let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) =
   let cfs,notations = List.split cfs in
   let cfs,priorities = List.split cfs in
   let coers,fs = List.split cfs in
@@ -576,14 +577,14 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
   let gr = match kind with
   | Class def ->
      let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
-     let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
+     let gr = declare_class finite def cum 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 (Universes.univ_inf_ind_from_universe_context ctx) idstruc
+	let ind = declare_structure Finite cum poly (Universes.univ_inf_ind_from_universe_context 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/vernac/record.mli b/vernac/record.mli
index ec5d2cf83..c43d833b0 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,8 @@ val declare_projections :
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
-  bool (** polymorphic?*) ->
+  Decl_kinds.cumulative_inductive_flag ->
+  Decl_kinds.polymorphic ->
   Univ.universe_info_ind (** universe and subtyping constraints *) ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
@@ -39,8 +40,8 @@ val declare_structure :
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
-  plident with_coercion * local_binder_expr list *
+  inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic *
+  Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d0f9c7de7..f130708c4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -526,7 +526,7 @@ let vernac_assumption locality poly (local, kind) l nl =
   let status = do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_record k poly finite struc binders sort nameopt cfs =
+let vernac_record cum k poly finite struc binders sort nameopt cfs =
   let const = match nameopt with
     | None -> add_prefix "Build_" (snd (fst (snd struc)))
     | Some (_,id as lid) ->
@@ -537,13 +537,13 @@ 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))
+    ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort))
 
 (** 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 poly lo finite indl =
+let vernac_inductive cum poly lo finite indl =
   if Dumpglob.dump () then
     List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
       match cstrs with
@@ -559,14 +559,14 @@ let vernac_inductive poly lo finite indl =
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
       user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
-      vernac_record (match b with Class _ -> Class false | _ -> b)
+      vernac_record cum (match b with Class _ -> Class false | _ -> b)
        poly finite id bl c oc fs
   | [ ( id , bl , c , Class _, 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 cum (Class true) poly finite id bl c None [f]
   | [ ( _ , _, _, Class _, Constructors _), [] ] ->
       user_err Pp.(str "Inductive classes not supported")
   | [ ( id , bl , c , Class _, _), _ :: _ ] ->
@@ -580,7 +580,7 @@ let vernac_inductive poly lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl poly lo finite
+    do_mutual_inductive indl cum poly lo finite
 
 let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
@@ -1365,6 +1365,14 @@ let _ =
       optwrite = Flags.make_universe_polymorphism }
 
 let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "inductive cumulativity";
+      optkey   = ["Inductive"; "Cumulativity"];
+      optread  = Flags.is_universe_polymorphism;
+      optwrite = Flags.make_universe_polymorphism }
+
+let _ =
   declare_int_option
     { optdepr  = false;
       optname  = "the level of inlining during functor application";
@@ -1933,7 +1941,7 @@ let interp ?proof ?loc locality poly c =
   | VernacEndProof e -> vernac_end_proof ?proof e
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
-  | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l
+  | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum 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
@@ -2083,6 +2091,12 @@ let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
   | Some b -> Flags.make_polymorphic_flag b; b
 
+let check_vernac_supports_cumulativity c p =
+  match p, c with
+  | None, _ -> ()
+  | Some _, (VernacInductive _ ) -> ()
+  | Some _, _ -> CErrors.error "This command does not support Cumulativity"
+
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)