Fix bugs and add an option for cumulativity

28 files changed, 1093 insertions, 155 deletions

diff --git a/API/API.mli b/API/API.mli
index a4ae6347c..a993b0277 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1095,6 +1095,7 @@ sig
         mind_nparams_rec : int;
         mind_params_ctxt : Context.Rel.t;
         mind_polymorphic : bool;
+        mind_cumulative : bool;
         mind_universes : Univ.universe_info_ind;
         mind_private : bool option;
         mind_typing_flags : Declarations.typing_flags;
@@ -1907,6 +1908,7 @@ end
 module Decl_kinds :
 sig
   type polymorphic = bool
+  type cumulative_inductive_flag = bool
   type recursivity_kind = Decl_kinds.recursivity_kind =
     | Finite
     | CoFinite
@@ -2388,7 +2390,7 @@ sig
   | VernacExactProof of Constrexpr.constr_expr
   | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) *
       inline * (plident list * Constrexpr.constr_expr) with_coercion list
-  | VernacInductive of Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
       Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
@@ -4743,7 +4745,9 @@ sig
   type one_inductive_impls = Command.one_inductive_impls
 
   val do_mutual_inductive :
-    (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> 
+    (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list ->
+    Decl_kinds.cumulative_inductive_flag -> 
+    Decl_kinds.polymorphic -> 
     Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit
 
   val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option ->
@@ -4767,7 +4771,9 @@ sig
     structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list
 
   val interp_mutual_inductive :
-    structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic ->
+    structured_inductive_expr -> Vernacexpr.decl_notation list ->
+    Decl_kinds.cumulative_inductive_flag ->
+    Decl_kinds.polymorphic ->
     Decl_kinds.private_flag -> Decl_kinds.recursivity_kind ->
     Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list
 
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
new file mode 100644
index 000000000..8409c7521
--- /dev/null
+++ b/ide/texmacspp.ml
@@ -0,0 +1,769 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Xml_datatype
+open Vernacexpr
+open Constrexpr
+open Names
+open Misctypes
+open Bigint
+open Decl_kinds
+open Extend
+open Libnames
+open Constrexpr_ops
+
+let unlock ?loc =
+  let start, stop = Option.cata Loc.unloc (0,0) loc in
+  (string_of_int start, string_of_int stop)
+
+let xmlWithLoc ?loc ename attr xml =
+  let start, stop = unlock ?loc in
+  Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
+
+let get_fst_attr_in_xml_list attr xml_list =
+  let attrs_list =
+    List.map (function
+      | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
+      | _ -> [])
+    xml_list in
+  match List.flatten attrs_list with
+  | [] -> (attr, "")
+  | l  -> (List.hd l)
+
+let backstep_loc xmllist =
+  let start_att = get_fst_attr_in_xml_list "begin" xmllist in
+  let stop_att =  get_fst_attr_in_xml_list "end" (List.rev xmllist) in
+  [start_att ; stop_att]
+
+let compare_begin_att xml1 xml2 =
+  let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
+  let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
+  match att1, att2 with
+  | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
+  | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
+  | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
+  | _ -> 0
+
+let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] []
+
+let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] []
+
+let xmlThm ?loc typ name xml =
+  xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml
+
+let xmlDef ?loc typ name xml =
+  xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml
+
+let xmlNotation ?loc attr name xml =
+  xmlWithLoc ?loc "notation" (("name", name) :: attr) xml
+
+let xmlReservedNotation ?loc attr name =
+  xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) []
+
+let xmlCst ?loc ?(attr=[]) name =
+  xmlWithLoc ?loc "constant" (("name", name) :: attr) []
+
+let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name =
+  xmlWithLoc ?loc "operator"
+    (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
+
+let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml
+
+let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml
+
+let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
+
+let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
+
+let xmlCase xml = Element("case", [], xml)
+
+let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
+
+let xmlWith xml = Element("with", [], xml)
+
+let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
+
+let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml
+
+let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
+
+let xmlFixpoint xml = Element("fixpoint", [], xml)
+
+let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml
+
+let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml
+
+let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml
+
+let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr []
+
+let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr []
+
+let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] []
+
+let xmlReference ref =
+  let name = Libnames.string_of_reference ref in
+  let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in
+  let b, e = string_of_int i, string_of_int j in
+  Element("reference",["name", name; "begin", b; "end", e] ,[])
+
+let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml
+let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml
+
+let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml
+let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr
+let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr
+
+let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml
+
+let xmlScope ?loc ?(attr=[]) action name xml =
+  xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml
+
+let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] []
+
+let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml
+
+let xmlSectionSubsetDescr name ssd =
+  Element("sectionsubsetdescr",["name",name],
+    [PCData (Proof_using.to_string ssd)])
+
+let xmlDeclareMLModule ?loc s =
+  xmlWithLoc ?loc "declarexmlmodule" []
+    (List.map (fun x -> Element("path",["value",x],[])) s)
+
+(* tactics *)
+let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml
+
+(* toplevel commands *)
+let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml
+
+let xmlTODO ?loc x =
+  xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+let string_of_name n =
+  match n with
+  | Anonymous -> "_"
+  | Name id -> Id.to_string id
+
+let string_of_glob_sort s =
+  match s with
+  | GProp -> "Prop"
+  | GSet -> "Set"
+  | GType _ -> "Type"
+
+let string_of_cast_sort c =
+  match c with
+  | CastConv _ -> "CastConv"
+  | CastVM _ -> "CastVM"
+  | CastNative _ -> "CastNative"
+  | CastCoerce -> "CastCoerce"
+
+let string_of_case_style s =
+  match s with
+  | LetStyle -> "Let"
+  | IfStyle -> "If"
+  | LetPatternStyle -> "LetPattern"
+  | MatchStyle -> "Match"
+  | RegularStyle -> "Regular"
+
+let attribute_of_syntax_modifier sm =
+match sm with
+  | SetItemLevel (sl, NumLevel n) ->
+      List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
+  | SetItemLevel (sl, NextLevel) ->
+      List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
+  | SetLevel i -> ["level", string_of_int i]
+  | SetAssoc a ->
+      begin match a with
+      | NonA -> ["",""]
+      | RightA -> ["associativity", "right"]
+      | LeftA -> ["associativity", "left"]
+      end
+  | SetEntryType (s, _) -> ["entrytype", s]
+  | SetOnlyPrinting -> ["onlyprinting", ""]
+  | SetOnlyParsing -> ["onlyparsing", ""]
+  | SetCompatVersion v -> ["compat", Flags.pr_version v]
+  | SetFormat (system, (loc, s)) ->
+      let start, stop = unlock ?loc in
+      ["format-"^system, s; "begin", start; "end", stop]
+
+let string_of_assumption_kind l a many =
+  match l, a, many with
+  | (Discharge, Logical,      true)  -> "Hypotheses"
+  | (Discharge, Logical,      false) -> "Hypothesis"
+  | (Discharge, Definitional, true)  -> "Variables"
+  | (Discharge, Definitional, false) -> "Variable"
+  | (Global,    Logical,      true)  -> "Axioms"
+  | (Global,    Logical,      false) -> "Axiom"
+  | (Global,    Definitional, true)  -> "Parameters"
+  | (Global,    Definitional, false) -> "Parameter"
+  | (Local,     Logical,      true)  -> "Local Axioms"
+  | (Local,     Logical,      false) -> "Local Axiom"
+  | (Local,     Definitional, true)  -> "Local Parameters"
+  | (Local,     Definitional, false) -> "Local Parameter"
+  | (Global,    Conjectural, _)      -> "Conjecture"
+  | ((Discharge | Local), Conjectural, _) -> assert false
+
+let rec pp_bindlist bl =
+  let tlist =
+    List.flatten
+        (List.map
+          (fun (loc_names, _, e) ->
+            let names =
+              (List.map
+                (fun (loc, name) ->
+                  xmlCst ?loc (string_of_name name)) loc_names) in
+            match e.CAst.v with
+              | CHole _ -> names
+              | _ -> names @ [pp_expr e])
+          bl) in
+  match tlist with
+    | [e] -> e
+    | l -> xmlTyped l
+and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
+  Element ("decl_notation", ["name", s], [pp_expr ce])
+and pp_local_binder lb = (* don't know what it is for now *)
+  match lb with
+  | CLocalDef ((loc, nam), ce, ty) ->
+      let attrs = ["name", string_of_name nam] in
+      let value = match ty with
+          Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
+        | None -> ce in
+      pp_expr ~attr:attrs value
+  | CLocalAssum (namll, _, ce) ->
+      let ppl =
+        List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in
+      xmlTyped (ppl @ [pp_expr ce])
+  | CLocalPattern _ ->
+      assert false
+and pp_local_decl_expr lde = (* don't know what it is for now *)
+  match lde with
+  | AssumExpr (_, ce)  -> pp_expr ce
+  | DefExpr (_, ce, _) -> pp_expr ce
+and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
+  (* inductive_expr *)
+  let b,e = Option.cata Loc.unloc (0,0) l in
+  let location = ["begin", string_of_int b; "end", string_of_int e] in
+  [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
+  begin match cl_or_rdexpr with
+  | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
+  | RecordDecl (_, ldewwwl) ->
+      List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
+  end @
+  begin match ceo with (* don't know what it is for now *)
+  | Some ce -> [pp_expr ce]
+  | None -> []
+  end @
+  (List.map pp_local_binder lbl)
+and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
+  let attrs =
+    match optid with
+    | None -> []
+    | Some (loc, id) ->
+        let start, stop = unlock ?loc in
+        ["begin", start; "end", stop ; "name", Id.to_string id] in
+  let kind, expr =
+    match roe with
+    | CStructRec -> "struct", []
+    | CWfRec e -> "rec", [pp_expr e]
+    | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
+    | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
+  Element ("recursion_order", ["kind", kind] @ attrs, expr)
+and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
+  (* fixpoint_expr *)
+  let start, stop = unlock ?loc in
+  let id = Id.to_string id in
+  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
+  (* fixpoint name *)
+  [pp_recursion_order_expr optid roe] @
+  (List.map pp_local_binder lbl) @
+  [pp_expr ce] @
+  begin match ceo with (* don't know what it is for now *)
+  | Some ce -> [pp_expr ce]
+  | None -> []
+  end
+and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
+  (* Nota: it is like fixpoint_expr without (optid, roe)
+   * so could be merged if there is no more differences *)
+  let start, stop = unlock ?loc in
+  let id = Id.to_string id in
+  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
+  (* cofixpoint name *)
+  (List.map pp_local_binder lbl) @
+  [pp_expr ce] @
+  begin match ceo with (* don't know what it is for now *)
+  | Some ce -> [pp_expr ce]
+  | None -> []
+  end
+and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id)
+and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
+and pp_cases_pattern_expr {loc ; CAst.v = cpe} =
+  match cpe with
+  | CPatAlias (cpe, id) ->
+      xmlApply ?loc
+        (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" ::
+          [pp_cases_pattern_expr cpe])
+  | CPatCstr (ref, None, cpel2) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "reference"
+           ~attr:["name", Libnames.string_of_reference ref] ::
+         [Element ("impargs", [], []);
+          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+  | CPatCstr (ref, Some cpel1, cpel2) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "reference"
+           ~attr:["name", Libnames.string_of_reference ref] ::
+         [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
+          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+  | CPatAtom optr ->
+      let attrs = match optr with
+        | None -> []
+        | Some r -> ["name", Libnames.string_of_reference r] in
+      xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: [])
+  | CPatOr cpel ->
+      xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel)
+  | CPatNotation (n, (subst_constr, subst_rec), cpel) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "notation" ::
+          [xmlOperator ?loc n;
+           Element ("subst", [],
+             [Element ("subterms", [],
+                List.map pp_cases_pattern_expr subst_constr);
+              Element ("recsubterms", [],
+                List.map
+                  (fun (cpel) ->
+                     Element ("recsubterm", [],
+                       List.map pp_cases_pattern_expr cpel))
+                subst_rec)]);
+           Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
+  | CPatPrim tok   -> pp_token ?loc tok
+  | CPatRecord rcl ->
+      xmlApply ?loc
+        (xmlOperator ?loc "record" ::
+           List.map (fun (r, cpe) ->
+             Element ("field",
+               ["reference", Libnames.string_of_reference r],
+               [pp_cases_pattern_expr cpe]))
+           rcl)
+  | CPatDelimiters (delim, cpe) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "delimiter" ~attr:["name", delim] ::
+          [pp_cases_pattern_expr cpe])
+  | CPatCast _ -> assert false
+and pp_case_expr (e, name, pat) =
+  match name, pat with
+  | None, None -> xmlScrutinee [pp_expr e]
+  | Some (loc, name), None ->
+      let start, stop= unlock ?loc in
+      xmlScrutinee ~attr:["name", string_of_name name;
+                          "begin", start; "end", stop] [pp_expr e]
+  | Some (loc, name), Some p ->
+      let start, stop= unlock ?loc in
+      xmlScrutinee ~attr:["name", string_of_name name;
+                          "begin", start; "end", stop]
+        [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
+  | None, Some p ->
+      xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
+and pp_branch_expr_list bel =
+  xmlWith
+    (List.map
+      (fun (_, (cpel, e)) ->
+        let ppcepl =
+          List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
+        let ppe = [pp_expr e] in
+        xmlCase (ppcepl @ ppe))
+     bel)
+and pp_token ?loc tok =
+  let tokstr =
+    match tok with
+    | String s -> PCData s
+    | Numeral n -> PCData (to_string n) in
+  xmlToken ?loc [tokstr]
+and pp_local_binder_list lbl =
+  let l = (List.map pp_local_binder lbl) in
+  Element ("recurse", (backstep_loc l), l)
+and pp_const_expr_list cel =
+  let l = List.map pp_expr cel in
+  Element ("recurse", (backstep_loc l), l)
+and pp_expr ?(attr=[]) { loc; CAst.v = e } =
+  match e with
+  | CRef (r, _) ->
+      xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r)
+  | CProdN (bl, e) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e])
+  | CApp ((_, hd), args) ->
+       xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
+  | CAppExpl ((_, r, _), args) ->
+       xmlApply ?loc ~attr
+         (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r)
+                 :: List.map pp_expr args)
+  | CNotation (notation,  ([],[],[])) ->
+       xmlOperator ?loc notation
+  | CNotation (notation,  (args, cell, lbll)) ->
+      let fmts = Notation.find_notation_extra_printing_rules notation in
+      let oper = xmlOperator ?loc notation ~pprules:fmts in
+      let cels = List.map pp_const_expr_list cell in
+      let lbls = List.map pp_local_binder_list lbll in
+      let args = List.map pp_expr args in
+      xmlApply ?loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
+  | CSort(s) ->
+      xmlOperator ?loc (string_of_glob_sort s)
+  | CDelimiters (scope, ce) ->
+      xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] ::
+        [pp_expr ce])
+  | CPrim tok -> pp_token ?loc tok
+  | CGeneralization (kind, _, e) ->
+      let kind= match kind with
+      | Explicit -> "explicit"
+      | Implicit -> "implicit" in
+      xmlApply ?loc
+        (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e])
+  | CCast (e, tc) ->
+      begin match tc with
+      | CastConv t | CastVM t |CastNative t ->
+          xmlApply ?loc
+            (xmlOperator ?loc ":" ~attr:["kind", (string_of_cast_sort tc)] ::
+             [pp_expr e; pp_expr t])
+      | CastCoerce   ->
+          xmlApply ?loc
+            (xmlOperator ?loc ":" ~attr:["kind", "CastCoerce"] ::
+             [pp_expr e])
+      end
+  | CEvar (ek, cel) ->
+      let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
+      xmlApply ?loc
+        (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] ::
+          ppcel)
+  | CPatVar id -> xmlPatvar ?loc (string_of_id id)
+  | CHole (_, _, _) -> xmlCst ?loc ~attr  "_"
+  | CIf (test, (_, ret), th, el) ->
+      let return = match ret with
+      | None -> []
+      | Some r -> [xmlReturn [pp_expr r]] in
+      xmlApply ?loc
+        (xmlOperator ?loc "if" ::
+          return @ [pp_expr th] @ [pp_expr el])
+  | CLetTuple (names, (_, ret), value, body) ->
+      let return = match ret with
+      | None -> []
+      | Some r -> [xmlReturn [pp_expr r]] in
+      xmlApply ?loc
+        (xmlOperator ?loc "lettuple" ::
+          return @
+          (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @
+          [pp_expr value; pp_expr body])
+  | CCases (sty, ret, cel, bel) ->
+      let return = match ret with
+      | None -> []
+      | Some r -> [xmlReturn [pp_expr r]] in
+      xmlApply ?loc
+        (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" ::
+          (return @
+           [Element ("scrutinees", [], List.map pp_case_expr cel)] @
+           [pp_branch_expr_list bel]))
+  | CRecord _ -> assert false
+  | CLetIn ((varloc, var), value, typ, body) ->
+      let value = match typ with
+        | Some t ->
+          CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t))
+        | None -> value in
+      xmlApply ?loc
+        (xmlOperator ?loc "let" ::
+         [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body])
+  | CLambdaN (bl, e) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e])
+  | CCoFix (_, _) -> assert false
+  | CFix (lid, fel) ->
+      xmlApply ?loc
+        (xmlOperator ?loc "fix" ::
+           List.flatten (List.map
+             (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
+             fel))
+
+let pp_comment c =
+  match c with
+  | CommentConstr e -> [pp_expr e]
+  | CommentString s -> [Element ("string", [], [PCData s])]
+  | CommentInt i    -> [PCData (string_of_int i)]
+
+let rec tmpp ?loc v =
+  match v with
+  (* Control *)
+  | VernacLoad (verbose,f) ->
+      xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] []
+  | VernacTime (loc,e) ->
+      xmlApply ?loc (Element("time",[],[]) ::
+                    [tmpp ?loc e])
+  | VernacRedirect (s, (loc,e)) ->
+      xmlApply ?loc (Element("redirect",["path", s],[]) ::
+                    [tmpp ?loc e])
+  | VernacTimeout (s,e) ->
+      xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) ::
+                    [tmpp ?loc e])
+  | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e])
+
+  (* Syntax *)
+  | VernacSyntaxExtension (_, ((_, name), sml)) ->
+      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+      xmlReservedNotation ?loc attrs name
+
+  | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name []
+  | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name []
+  | VernacDelimiters (name,Some tag) ->
+      xmlScope ?loc "delimit" name ~attr:["delimiter",tag] []
+  | VernacDelimiters (name,None) ->
+      xmlScope ?loc "undelimit" name ~attr:[] []
+  | VernacInfix (_,((_,name),sml),ce,sn) ->
+      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+      let sc_attr =
+        match sn with
+        | Some scope -> ["scope", scope]
+        | None -> [] in
+      xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce]
+  | VernacNotation (_, ce, (lstr, sml), sn) ->
+      let name = snd lstr in
+      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+      let sc_attr =
+        match sn with
+        | Some scope -> ["scope", scope]
+        | None -> [] in
+      xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce]
+  | VernacBindScope _ as x -> xmlTODO ?loc x
+  | VernacNotationAddFormat _ as x -> xmlTODO ?loc x
+  | VernacUniverse _
+  | VernacConstraint _
+  | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x
+  (* Gallina *)
+  | VernacDefinition (ldk, ((_,id),_), de) ->
+      let l, dk =
+        match ldk with
+        | Some l, dk -> (l, dk)
+        | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
+      let e =
+        match de with
+        | ProveBody (_, ce) -> ce
+        | DefineBody (_, Some _, ce, None) -> ce
+        | DefineBody (_, None  , ce, None) -> ce
+        | DefineBody (_, Some _, ce, Some _) -> ce
+        | DefineBody (_, None  , ce, Some _) -> ce in
+      let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
+      let str_id = Id.to_string id in
+      (xmlDef ?loc str_dk str_id [pp_expr e])
+  | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
+      let str_tk = Kindops.string_of_theorem_kind tk in
+      let str_id = Id.to_string id in
+      (xmlThm ?loc str_tk str_id [pp_expr statement])
+  | VernacStartTheoremProof _ as x -> xmlTODO ?loc x
+  | VernacEndProof pe ->
+      begin
+        match pe with
+        | Admitted -> xmlQed ?loc ?attr:None
+        | Proved (_, Some ((_, id), Some tk)) ->
+            let nam = Id.to_string id in
+            let typ = Kindops.string_of_theorem_kind tk in
+            xmlQed ?loc ~attr:["name", nam; "type", typ]
+        | Proved (_, Some ((_, id), None)) ->
+            let nam = Id.to_string id in
+            xmlQed ?loc ~attr:["name", nam]
+        | Proved _ -> xmlQed ?loc ?attr:None
+      end
+  | VernacExactProof _ as x -> xmlTODO ?loc x
+  | VernacAssumption ((l, a), _, sbwcl) ->
+      let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
+      let many =
+        List.length (List.flatten (List.map fst binders)) > 1 in
+      let exprs =
+        List.flatten (List.map pp_simple_binder binders) in
+      let l = match l with Some x -> x | None -> Decl_kinds.Global in
+      let kind = string_of_assumption_kind l a many in
+      xmlAssumption ?loc kind exprs
+  | VernacInductive (_, _, _, iednll) ->
+      let kind =
+        let (_, _, _, k, _), _ = List.hd iednll in
+	  begin
+            match k with
+            | Record -> "Record"
+            | Structure -> "Structure"
+            | Inductive_kw -> "Inductive"
+            | CoInductive -> "CoInductive"
+            | Class _ -> "Class"
+            | Variant -> "Variant"
+          end in
+      let exprs =
+        List.flatten (* should probably not be flattened *)
+          (List.map
+            (fun (ie, dnl) -> (pp_inductive_expr ie) @
+                              (List.map pp_decl_notation dnl)) iednll) in
+      xmlInductive ?loc kind exprs
+  | VernacFixpoint (_, fednll) ->
+      let exprs =
+        List.flatten (* should probably not be flattened *)
+          (List.map
+            (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
+                              (List.map pp_decl_notation dnl)) fednll) in
+      xmlFixpoint exprs
+  | VernacCoFixpoint (_, cfednll) ->
+      (* Nota: it is like VernacFixpoint without so could be merged *)
+      let exprs =
+        List.flatten (* should probably not be flattened *)
+          (List.map
+            (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
+                              (List.map pp_decl_notation dnl)) cfednll) in
+      xmlCoFixpoint exprs
+  | VernacScheme _ as x -> xmlTODO ?loc x
+  | VernacCombinedScheme _ as x -> xmlTODO ?loc x
+
+  (* Gallina extensions *)
+  | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id)
+  | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id)
+  | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x
+  | VernacRequire (from, import, l) ->
+      let import = match import with
+      | None -> []
+      | Some true -> ["export","true"]
+      | Some false -> ["import","true"]
+      in
+      let from = match from with
+      | None -> []
+      | Some r -> ["from", Libnames.string_of_reference r]
+      in
+      xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacImport (true,l) ->
+      xmlImport ?loc ~attr:["export","true"] (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacImport (false,l) ->
+      xmlImport ?loc (List.map (fun ref -> xmlReference ref) l)
+  | VernacCanonical r ->
+      let attr =
+        match r with
+        | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
+        | AN (Ident (_, id)) -> ["id", Id.to_string id]
+        | ByNotation (_, (s, _)) -> ["notation", s] in
+      xmlCanonicalStructure ?loc attr
+  | VernacCoercion _ as x -> xmlTODO ?loc x
+  | VernacIdentityCoercion _ as x -> xmlTODO ?loc x
+
+  (* Type classes *)
+  | VernacInstance _ as x -> xmlTODO ?loc x
+
+  | VernacContext _ as x -> xmlTODO ?loc x
+
+  | VernacDeclareInstances _ as x -> xmlTODO ?loc x
+
+  | VernacDeclareClass _ as x -> xmlTODO ?loc x
+
+  (* Modules and Module Types *)
+  | VernacDeclareModule _ as x -> xmlTODO ?loc x
+  | VernacDefineModule _ as x -> xmlTODO ?loc x
+  | VernacDeclareModuleType _ as x -> xmlTODO ?loc x
+  | VernacInclude _ as x -> xmlTODO ?loc x
+
+  (* Solving *)
+
+  | (VernacSolveExistential _) as x ->
+      xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+  (* Auxiliary file and library management *)
+  | VernacAddLoadPath (recf,name,None) ->
+      xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] []
+  | VernacAddLoadPath (recf,name,Some dp) ->
+      xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name]
+        [PCData (Names.DirPath.to_string dp)]
+  | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] []
+  | VernacAddMLPath (recf,name) ->
+      xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] []
+  | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl
+  | VernacChdir _ as x -> xmlTODO ?loc x
+
+  (* State management *)
+  | VernacWriteState _ as x -> xmlTODO ?loc x
+  | VernacRestoreState _ as x -> xmlTODO ?loc x
+
+  (* Resetting *)
+  | VernacResetName _ as x -> xmlTODO ?loc x
+  | VernacResetInitial as x -> xmlTODO ?loc x
+  | VernacBack _ as x -> xmlTODO ?loc x
+  | VernacBackTo _ -> PCData "VernacBackTo"
+
+  (* Commands *)
+  | VernacCreateHintDb _ as x -> xmlTODO ?loc x
+  | VernacRemoveHints _ as x -> xmlTODO ?loc x
+  | VernacHints _ as x -> xmlTODO ?loc x
+  | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
+      let name = Id.to_string name in
+      let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
+      xmlNotation ?loc attrs name [pp_expr ce]
+  | VernacDeclareImplicits _ as x -> xmlTODO ?loc x
+  | VernacArguments _ as x -> xmlTODO ?loc x
+  | VernacArgumentsScope _ as x -> xmlTODO ?loc x
+  | VernacReserve _ as x -> xmlTODO ?loc x
+  | VernacGeneralizable _ as x -> xmlTODO ?loc x
+  | VernacSetOpacity _ as x -> xmlTODO ?loc x
+  | VernacSetStrategy _ as x -> xmlTODO ?loc x
+  | VernacUnsetOption _ as x -> xmlTODO ?loc x
+  | VernacSetOption _ as x -> xmlTODO ?loc x
+  | VernacSetAppendOption _ as x -> xmlTODO ?loc x
+  | VernacAddOption _ as x -> xmlTODO ?loc x
+  | VernacRemoveOption _ as x -> xmlTODO ?loc x
+  | VernacMemOption _ as x -> xmlTODO ?loc x
+  | VernacPrintOption _ as x -> xmlTODO ?loc x
+  | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e]
+  | VernacGlobalCheck _ as x -> xmlTODO ?loc x
+  | VernacDeclareReduction _ as x -> xmlTODO ?loc x
+  | VernacPrint _ as x -> xmlTODO ?loc x
+  | VernacSearch _ as x -> xmlTODO ?loc x
+  | VernacLocate _ as x -> xmlTODO ?loc x
+  | VernacRegister _ as x -> xmlTODO ?loc x
+  | VernacComments (cl) ->
+      xmlComment ?loc (List.flatten (List.map pp_comment cl))
+
+  (* Stm backdoor *)
+  | VernacStm _ as x -> xmlTODO ?loc x
+
+  (* Proof management *)
+  | VernacGoal _ as x -> xmlTODO ?loc x
+  | VernacAbort _ as x -> xmlTODO ?loc x
+  | VernacAbortAll -> PCData "VernacAbortAll"
+  | VernacRestart as x -> xmlTODO ?loc x
+  | VernacUndo _ as x -> xmlTODO ?loc x
+  | VernacUndoTo _ as x -> xmlTODO ?loc x
+  | VernacBacktrack _ as x -> xmlTODO ?loc x
+  | VernacFocus _ as x -> xmlTODO ?loc x
+  | VernacUnfocus as x -> xmlTODO ?loc x
+  | VernacUnfocused as x -> xmlTODO ?loc x
+  | VernacBullet _ as x -> xmlTODO ?loc x
+  | VernacSubproof _ as x -> xmlTODO ?loc x
+  | VernacEndSubproof as x -> xmlTODO ?loc x
+  | VernacShow _ as x -> xmlTODO ?loc x
+  | VernacCheckGuard as x -> xmlTODO ?loc x
+  | VernacProof (tac,using) ->
+      let tac = None (** FIXME *) in
+      let using = Option.map (xmlSectionSubsetDescr "using") using in
+      xmlProof ?loc (Option.List.(cons tac (cons using [])))
+  | VernacProofMode name -> xmlProofMode ?loc name
+
+  (* Toplevel control *)
+  | VernacToplevelControl _ as x -> xmlTODO ?loc x
+
+  (* For extension *)
+  | VernacExtend _ as x ->
+      xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+  (* Flags *)
+  | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e])
+  | VernacLocal (b,e) ->
+      xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) ::
+                    [tmpp ?loc e])
+
+let tmpp ?loc v =
+  match tmpp ?loc v with
+  | Element("ltac",_,_) as x -> x
+  | xml -> xmlGallina ?loc [xml]
diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml
index 8254b1b80..c15c00988 100644
--- a/intf/decl_kinds.ml
+++ b/intf/decl_kinds.ml
@@ -14,7 +14,9 @@ type binding_kind = Explicit | Implicit
 
 type polymorphic = bool
 
-type private_flag = bool 
+type private_flag = bool
+
+type cumulative_inductive_flag = bool
 
 type theorem_kind =
   | Theorem
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index cabd06735..26a6db4ec 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -336,7 +336,7 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
       inline * (plident list * constr_expr) with_coercion list
-  | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_flag * 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/kernel/declarations.ml b/kernel/declarations.ml
index 1bb1e885f..ae4732456 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -188,6 +188,8 @@ type mutual_inductive_body = {
 
     mind_polymorphic : bool; (** Is it polymorphic or not *)
 
+    mind_cumulative : bool; (** Is it cumulative or not *)
+
     mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 883896652..1d91b2d41 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -267,6 +267,7 @@ let subst_mind_body sub mib =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_polymorphic = mib.mind_polymorphic;
+    mind_cumulative = mib.mind_cumulative;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 97c28025a..9c17346f2 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -49,7 +49,8 @@ type mutual_inductive_entry = {
   mind_entry_finite : Decl_kinds.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list;
-  mind_entry_polymorphic : bool; 
+  mind_entry_polymorphic : bool;
+  mind_entry_cumulative : bool;
   mind_entry_universes : Univ.universe_info_ind;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a4c7a0573..5cfcbba60 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -392,7 +392,7 @@ let typecheck_inductive env mie =
   in
   (* Check that the subtyping information inferred for inductive types in the block is correct. *)
   (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
-  let () = check_subtyping mie paramsctxt env_arities inds
+  let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds
   in (env_arities, env_ar_par, paramsctxt, inds)
 
 (************************************************************************)
@@ -864,7 +864,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
-let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
@@ -969,6 +969,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_polymorphic = p;
+      mind_cumulative = cum;
       mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp);
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
@@ -984,7 +985,7 @@ let check_inductive env kn mie =
   let chkpos = (Environ.typing_flags env).check_guarded 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_polymorphic mie.mind_entry_private
+    build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
       env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 33dd53a5b..ea583fdac 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -191,7 +191,10 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    leq_inductives : flex:bool -> Univ.UInfoInd.t -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
+      Univ.Instance.t -> int -> 'a -> 'a;
+    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
+      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
@@ -207,9 +210,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
+  
+let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
+  (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
 
-let compare_leq_inductives ~flex uinfind u u' (s, check) =
-  (check.leq_inductives ~flex uinfind u u' s, check)
+let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
+  (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -487,64 +493,31 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   | _ -> raise NotConvertible)
        
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
-
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-      if eq_ind ind1 ind2
-      then
-        begin
-          let fall_back () =
-            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-          in
-          let mind = Environ.lookup_mind (fst ind1) env in
-          if mind.Declarations.mind_polymorphic then
-            begin
-              let num_param_arity =
-                mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs
-              in
-              if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
-                fall_back ()
-              else
-                begin
-                  let uinfind = mind.Declarations.mind_universes in
-                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-                  let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
-                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-                end
-            end
+      if eq_ind ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) env in
+        let cuniv =
+          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+            convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
+              u2 (CClosure.stack_args_size v2) cuniv
           else
-            fall_back ()
-        end
+            convert_instances ~flex:false u1 u2 cuniv
+        in
+        convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-      if Int.equal j1 j2 && eq_ind ind1 ind2
-      then
-        begin
-          let fall_back () =
-            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-          in
-          let mind = Environ.lookup_mind (fst ind1) env in
-          if mind.Declarations.mind_polymorphic then
-            begin
-              let num_cnstr_args =
-                let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in
-                nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1)
-              in
-              if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then
-                fall_back ()
-              else
-                begin (* we consider subtyping for constructors. *)
-                  let uinfind = mind.Declarations.mind_universes in
-                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-                  let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in
-                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-                end
-            end
+      if Int.equal j1 j2 && eq_ind ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) env in
+        let cuniv =
+          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+            convert_constructors
+              (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
+              u2 (CClosure.stack_args_size v2) cuniv
           else
-            fall_back ()
-        end
+            convert_instances ~flex:false u1 u2 cuniv
+        in
+        convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -659,24 +632,79 @@ let check_convert_instances ~flex u u' univs =
   if UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
-let check_leq_inductives ~flex uinfind u u' univs =
+(* general conversion and inference functions *)
+let infer_check_conv_inductives
+    infer_check_convert_instances
+    infer_check_inductive_instances
+    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+  if mind.Declarations.mind_polymorphic then
+    let num_param_arity =
+      mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      infer_check_convert_instances ~flex:false u1 u2 univs
+    else
+      let uinfind = mind.Declarations.mind_universes in
+      infer_check_inductive_instances cv_pb uinfind u1 u2 univs
+  else infer_check_convert_instances ~flex:false u1 u2 univs
+
+let infer_check_conv_constructors
+    infer_check_convert_instances
+    infer_check_inductive_instances
+    (mind, ind, cns) u1 sv1 u2 sv2 univs =
+  if mind.Declarations.mind_polymorphic then
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+    in
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      infer_check_convert_instances ~flex:false u1 u2 univs
+    else
+      let uinfind = mind.Declarations.mind_universes in
+      infer_check_inductive_instances CONV uinfind u1 u2 univs
+  else infer_check_convert_instances ~flex:false u1 u2 univs
+
+let check_inductive_instances cv_pb uinfind u u' univs =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
   let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
-    begin
-     let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
-     if UGraph.check_constraints comp_cst univs then univs
-     else raise NotConvertible
-    end
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    if (UGraph.check_constraints comp_cst univs) then univs
+    else raise NotConvertible
+
+let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+  infer_check_conv_inductives
+    check_convert_instances
+    check_inductive_instances
+    cv_pb ind u1 sv1 u2 sv2 univs
+
+let check_conv_constructors cns u1 sv1 u2 sv2 univs =
+  infer_check_conv_constructors
+    check_convert_instances
+    check_inductive_instances
+    cns u1 sv1 u2 sv2 univs
 
 let checked_universes =
   { compare = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
-    leq_inductives = check_leq_inductives }
+    conv_inductives = check_conv_inductives;
+    conv_constructors = check_conv_constructors}
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -718,21 +746,45 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) =
+let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
   let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
-     let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
-     (univs, Univ.Constraint.union cstrs comp_cst)
-
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    (univs, Univ.Constraint.union cstrs comp_cst)
+
+
+let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+  infer_check_conv_inductives
+    infer_convert_instances
+    infer_inductive_instances
+    cv_pb ind u1 sv1 u2 sv2 univs
+
+let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
+  infer_check_conv_constructors
+    infer_convert_instances
+    infer_inductive_instances
+    cns u1 sv1 u2 sv2 univs
+    
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances;
-    leq_inductives = infer_leq_inductives }
+    conv_inductives = infer_conv_inductives;
+    conv_constructors = infer_conv_constructors}
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 72f0ecffd..b6d88c2b9 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,12 +36,13 @@ type 'a extended_conversion_function =
 type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = 
-  { (* Might raise NotConvertible or UnivInconsistency *)
+  { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
-    compare_instances: flex:bool -> 
-		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    leq_inductives : flex:bool -> Univ.UInfoInd.t ->
-                     Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
+      Univ.Instance.t -> int -> 'a -> 'a;
+    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
+      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
diff --git a/lib/flags.ml b/lib/flags.ml
index 13539bced..46bbba8e5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -163,6 +163,10 @@ let use_polymorphic_flag () =
 let make_polymorphic_flag b =
   local_polymorphic_flag := Some b
 
+let inductive_cumulativity = ref false
+let make_inductive_cumulativity b = inductive_cumulativity := b
+let is_inductive_cumulativity () = !inductive_cumulativity
+
 (** [program_mode] tells that Program mode has been activated, either
     globally via [Set Program] or locally via the Program command prefix. *)
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 0026aba2e..5e78f0a04 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -119,6 +119,10 @@ val is_universe_polymorphism : unit -> bool
 val make_polymorphic_flag : bool -> unit
 val use_polymorphic_flag : unit -> bool
 
+(** Global inductive cumulativity flag. *)
+val make_inductive_cumulativity : bool -> unit
+val is_inductive_cumulativity : unit -> bool
+
 val warn : bool ref
 val make_warn : bool -> unit
 val if_warn : ('a -> unit) -> 'a -> unit
diff --git a/library/declare.ml b/library/declare.ml
index bf5313545..e2b726f45 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -352,13 +352,14 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
+  mind_entry_cumulative = false;
   mind_entry_universes = Univ.UInfoInd.empty;
   mind_entry_private = None;
 })
 
 (* reinfer subtyping constraints for inductive after section is dischared. *)
 let infer_inductive_subtyping (pth, mind_ent) = 
-  if mind_ent.mind_entry_polymorphic then
+  if mind_ent.mind_entry_polymorphic && mind_ent.mind_entry_cumulative then
     begin
       let env = Global.env () in
       let env' =
@@ -370,7 +371,6 @@ let infer_inductive_subtyping (pth, mind_ent) =
     end
   else (pth, mind_ent)
 
-
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
 let inInductive : inductive_obj -> obj =
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b605a44c8..e6b28b1d8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -162,11 +162,16 @@ GEXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((Some Discharge, Definition), (id, None), b)
       (* Gallina inductive declarations *)
-      | priv = private_token; f = finite_token;
+      | cum = cumulativity_token; priv = private_token; f = finite_token;
         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)
+          let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
+	  let cum =
+	    match cum with
+	      Some b -> b
+	    | None -> Flags.is_inductive_cumulativity ()
+	  in
+          VernacInductive (cum, priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -234,6 +239,9 @@ GEXTEND Gram
       | IDENT "Structure" -> (Structure,BiFinite)
       | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
+  cumulativity_token:
+    [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ]
+  ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
   ;
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0e2ca4900..db2af2be5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1459,7 +1459,9 @@ 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 rel_inds (Flags.is_universe_polymorphism ()) false false))
+      Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
@@ -1470,7 +1472,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(false,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1485,7 +1487,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(false,false,Decl_kinds.Finite,repacked_rel_inds))
 	    ++ fnl () ++
 	    CErrors.print reraise
 	in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c75f7f868..ba88563d3 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -880,7 +880,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   (* Declare inductive *)
   let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
   let mie,pl,impls = Command.interp_mutual_inductive indl []
-          false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
+          false (* non-cumulative *) 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 pl impls)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ea22c3708..be2fd8129 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -494,6 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             if mind.Declarations.mind_polymorphic then
               begin
                 let num_param_arity =
+                  (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *)
                   mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
                 if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then
@@ -521,6 +522,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
             begin
               let num_cnstr_args =
                 let nparamsctxt =
+                  (* Context.Rel.length mind.Declarations.mind_params_ctxt *)
                   mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs
                 in
                 nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e374f7b3b..2040acba7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1361,24 +1361,68 @@ let sigma_compare_instances ~flex i0 i1 sigma =
      | Univ.UniverseInconsistency _ ->
 	raise Reduction.NotConvertible
 
-let sigma_leq_inductives ~flex uinfind i0 i1 sigma =
+let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
   let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
-     let comp_subst = (Univ.Instance.append i0 i1) in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
-     try Evd.add_constraints sigma comp_cst
-     with Evd.UniversesDiffer
-        | Univ.UniverseInconsistency _ ->
-	    raise Reduction.NotConvertible
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        Reduction.CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | Reduction.CUMUL -> comp_cst
+    in
+    try Evd.add_constraints sigma comp_cst
+    with Evd.UniversesDiffer
+       | Univ.UniverseInconsistency _ ->
+      raise Reduction.NotConvertible
+
+let sigma_conv_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
+  try sigma_compare_instances ~flex:false u1 u2 sigma with
+    Reduction.NotConvertible ->
+    if mind.Declarations.mind_polymorphic then
+      let num_param_arity =
+        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+      in
+      if not (num_param_arity = sv1 && num_param_arity = sv2) then
+        raise Reduction.NotConvertible
+      else
+        let uinfind = mind.Declarations.mind_universes in
+        sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma
+    else raise Reduction.NotConvertible
+
+let sigma_conv_constructors
+    (mind, ind, cns) u1 sv1 u2 sv2 sigma =
+  try sigma_compare_instances ~flex:false u1 u2 sigma with
+    Reduction.NotConvertible ->
+    if mind.Declarations.mind_polymorphic then
+      let num_cnstr_args =
+        let nparamsctxt =
+          mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+          (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+        nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+      in
+      if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+        raise Reduction.NotConvertible
+      else
+        let uinfind = mind.Declarations.mind_universes in
+        sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma
+    else raise Reduction.NotConvertible
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances;
-    Reduction.leq_inductives = sigma_leq_inductives }
+    Reduction.conv_inductives = sigma_conv_inductives;
+    Reduction.conv_constructors = sigma_conv_constructors}
 
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9d28bc4f8..6a47c308d 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -727,7 +727,7 @@ open Decl_kinds
         let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
         return (hov 2 (pr_assumption_token (n > 1) stre ++
                        pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
-      | VernacInductive (p,f,l) ->
+      | VernacInductive (cum, p,f,l) ->
         let pr_constructor (coe,(id,c)) =
           hov 2 (pr_lident id ++ str" " ++
                    (if coe then str":>" else str":") ++
@@ -754,13 +754,17 @@ open Decl_kinds
         in
         let key =
           let (_,_,_,k,_),_ = List.hd l in
-          match k with Record -> "Record" | Structure -> "Structure"
-            | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-            | Class _ -> "Class" | Variant -> "Variant"
+          let kind =
+            match k with Record -> "Record" | Structure -> "Structure"
+                       | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+                       | Class _ -> "Class" | Variant -> "Variant"
+          in
+          let cm = if cum then "Cumulative" else "NonCumulative" in
+          cm ^ " " ^ kind
         in
         return (
           hov 1 (pr_oneind key (List.hd l)) ++
-            (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
+          (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
         )
 
       | VernacFixpoint (local, recs) ->
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 471e05e45..87d9e411a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -142,7 +142,7 @@ let rec classify_vernac e =
         let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) 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/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index e3b5e9435..a497e7a98 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function
 
 Open Scope function_scope.
 
+Set Printing Universes. Set Printing All.
+
 Inductive paths {A : Type} (a : A) : A -> Type :=
   idpath : paths a a.
 
@@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism.
 
 Delimit Scope category_scope with category.
 Delimit Scope object_scope with object.
-
+Set Printing Universes.
+Set Printing All.
 Record PreCategory :=
   Build_PreCategory' {
       object :> Type;
@@ -1069,8 +1072,10 @@ Section Adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-  Let Adjunction_Type := 
-    Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).
+(*  Let Adjunction_Type := 
+    Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).*)
+
+  Set Printing All. Set Printing Universes.
 
   Record AdjunctionHom :=
     {
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 3e90825ab..f57cbcc2b 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -316,26 +316,6 @@ Module Hurkens'.
 
 Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
 
-Section test_letin_subtyping.
-  Universe i j k i' j' k'.
-  Constraint j < j'.
-
-  Context (W : Type) (X : box@{i j k} W).
-  Definition Y := X : box@{i' j' k'} W.
-
-  Universe i1 j1 k1 i2 j2 k2.
-  Constraint i1 < i2, k2 < k1.
-  Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}.
-  Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}.
-  Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'.
-  Proof.
-    Set Printing All. Set Printing Universes.
-    cbv.
-    reflexivity.
-  Qed.
-
-End test_letin_subtyping.
-
 Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
@@ -372,3 +352,35 @@ Module Anonymous.
   Check collapsethemiddle@{_ _}.
 
 End Anonymous.
+
+Module F.
+  Context {A B : Type}.
+  Definition foo : Type := B.
+End F.
+
+Set Universe Polymorphism.
+
+Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Section test_letin_subtyping.
+  Universe i j k i' j' k'.
+  Constraint j < j'.
+
+  Context (W : Type) (X : box@{i j k} W).
+  Definition Y := X : box@{i' j' k'} W.
+
+  Universe i1 j1 k1 i2 j2 k2.
+  Constraint i1 < i2.
+  Constraint k2 < k1.
+  Context (V : Type).
+
+  Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}.
+  Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}.
+  Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'.
+  Proof.
+    Set Printing All. Set Printing Universes.
+    cbv.
+    reflexivity.
+  Qed.
+
+End test_letin_subtyping.
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). *)