Merge remote-tracking branch 'upstream/trunk' into trunk

19 files changed, 276 insertions, 248 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8e6a0f6a72..2e8ebb8531 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -114,8 +114,8 @@ let instance_hook k info global imps ?hook cst =
 let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
   let evm = 
-    let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
-				 (Universes.universes_of_constr term) in
+    let levels = Univ.LSet.union (Univops.universes_of_constr termtype) 
+				 (Univops.universes_of_constr term) in
     Evd.restrict_universe_context evm levels 
   in
   let pl, uctx = Evd.universe_context ?names:pl evm in
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term)));
+                      Refine.refine ~typecheck:false (fun evm -> (evm,EConstr.of_constr (Option.get term)));
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
@@ -417,9 +417,11 @@ let context poly l =
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
         let hook = Lemmas.mk_hook (fun _ gr -> gr) in
-        let _ = Command.declare_definition id decl entry [] [] hook in
+        let _ = DeclareDef.declare_definition id decl entry [] [] hook in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
-      let () = uctx := Univ.ContextSet.empty in
 	status && nstatus
-  in List.fold_left fn true (List.rev ctx)
+  in 
+  if Lib.sections_are_opened () then
+    Declare.declare_universe_context poly !uctx;
+  List.fold_left fn true (List.rev ctx)
diff --git a/vernac/command.ml b/vernac/command.ml
index b1425d7034..fd49e53243 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -106,7 +106,7 @@ let interp_definition pl bl p red_option c ctypopt =
 	let c = EConstr.Unsafe.to_constr c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
         let body = nf (it_mkLambda_or_LetIn c ctx) in
-	let vars = Universes.universes_of_constr body in
+	let vars = Univops.universes_of_constr body in
 	let evd = Evd.restrict_universe_context !evdref vars in
 	let pl, uctx = Evd.universe_context ?names:pl evd in
  	imps1@(Impargs.lift_implicits nb_args imps2), pl,
@@ -131,8 +131,8 @@ let interp_definition pl bl p red_option c ctypopt =
         in
 	if not (try List.for_all chk imps2 with Not_found -> false)
 	then warn_implicits_in_term ();
-        let vars = Univ.LSet.union (Universes.universes_of_constr body) 
-          (Universes.universes_of_constr typ) in
+        let vars = Univ.LSet.union (Univops.universes_of_constr body) 
+          (Univops.universes_of_constr typ) in
         let ctx = Evd.restrict_universe_context !evdref vars in
 	let pl, uctx = Evd.universe_context ?names:pl ctx in
 	imps1@(Impargs.lift_implicits nb_args impsty), pl,
@@ -145,59 +145,6 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
-let warn_local_declaration =
-  CWarnings.create ~name:"local-declaration" ~category:"scope"
-         (fun (id,kind) ->
-          pr_id id ++ strbrk " is declared as a local " ++ str kind)
-
-let get_locality id ~kind = function
-| Discharge ->
-  (** If a Let is defined outside a section, then we consider it as a local definition *)
-   warn_local_declaration (id,kind);
-  true
-| Local -> true
-| Global -> false
-
-let declare_global_definition ident ce local k pl imps =
-  let local = get_locality ident ~kind:"definition" local in
-  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
-  let gr = ConstRef kn in
-  let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
-  let () = definition_message ident in
-  gr
-
-let declare_definition_hook = ref ignore
-let set_declare_definition_hook = (:=) declare_definition_hook
-let get_declare_definition_hook () = !declare_definition_hook
-
-let warn_definition_not_visible =
-  CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
-         (fun ident ->
-          strbrk "Section definition " ++
-            pr_id ident ++ strbrk " is not visible from current goals")
-
-let declare_definition ident (local, p, k) ce pl imps hook =
-  let fix_exn = Future.fix_exn_of ce.const_entry_body in
-  let () = !declare_definition_hook ce in
-  let r = match local with
-  | Discharge when Lib.sections_are_opened () ->
-    let c = SectionLocalDef ce in
-    let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
-    let () = definition_message ident in
-    let gr = VarRef ident in
-    let () = maybe_declare_manual_implicits false gr imps in
-    let () = if Pfedit.refining () then
-	       warn_definition_not_visible ident
-    in
-    gr
-  | Discharge | Local | Global ->
-    declare_global_definition ident ce local k pl imps in
-  Lemmas.call_hook fix_exn hook local r
-
-let _ = Obligations.declare_definition_ref :=
-       (fun i k c imps hook -> declare_definition i k c [] imps hook)
-
 let do_definition ident k pl bl red_option c ctypopt hook =
   let (ce, evd, pl', imps as def) =
     interp_definition pl bl (pi2 k) red_option c ctypopt
@@ -220,7 +167,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ident k ce pl' imps
+      ignore(DeclareDef.declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -233,7 +180,7 @@ match local with
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let () =
-    if not !Flags.quiet && Pfedit.refining () then
+    if not !Flags.quiet && Proof_global.there_are_pending_proofs () then
     Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
     strbrk " is not visible from current goals")
   in
@@ -243,7 +190,7 @@ match local with
   (r,Univ.Instance.empty,true)
 
 | Global | Local | Discharge ->
-  let local = get_locality ident ~kind:"axiom" local in
+  let local = DeclareDef.get_locality ident ~kind:"axiom" local in
   let inl = match nl with
     | NoInline -> None
     | DefaultInline -> Some (Flags.get_inline_level())
@@ -329,7 +276,7 @@ let do_assumptions_bound_univs coe kind nl id pl c =
   let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
   let ty = EConstr.Unsafe.to_constr ty in
   let ty = nf ty in
-  let vars = Universes.universes_of_constr ty in
+  let vars = Univops.universes_of_constr ty in
   let evd = Evd.restrict_universe_context !evdref vars in
   let pl, uctx = Evd.universe_context ?names:pl evd in
   let uctx = Univ.ContextSet.of_context uctx in
@@ -573,7 +520,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
@@ -649,16 +596,27 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
+  let univs =
+    if poly then
+      if cum then
+        Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
+      else Polymorphic_ind_entry uctx
+    else
+      Monomorphic_ind_entry uctx
+  in
   (* Build the mutual inductive entry *)
-  { mind_entry_params = List.map prepare_param ctx_params;
-    mind_entry_record = None;
-    mind_entry_finite = finite;
-    mind_entry_inds = entries;
-    mind_entry_polymorphic = poly;
-    mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = uctx;
-  },
-    pl, impls
+  let mind_ent =
+    { mind_entry_params = List.map prepare_param ctx_params;
+      mind_entry_record = None;
+      mind_entry_finite = finite;
+      mind_entry_inds = entries;
+      mind_entry_private = if prv then Some false else None;
+      mind_entry_universes = univs;
+    }
+  in
+  (if poly && cum then
+      Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
+   else mind_ent), pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -742,10 +700,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 *)
@@ -865,13 +823,6 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
-  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
-
-let _ = Obligations.declare_fix_ref :=
-  (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
-
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
   let names = List.map (fun id -> Name id) fixnames in
@@ -1208,14 +1159,14 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let env = Global.env() in
     let indexes = search_guard env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-    let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+    let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
+    ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1240,13 +1191,13 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-    let vars = Universes.universes_of_constr (List.hd fixdecls) in
+    let vars = Univops.universes_of_constr (List.hd fixdecls) in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
+    ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
diff --git a/vernac/command.mli b/vernac/command.mli
index 9bbc2fdac1..1887885de9 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -15,7 +15,6 @@ open Vernacexpr
 open Constrexpr
 open Decl_kinds
 open Redexpr
-open Pfedit
 
 (** This file is about the interpretation of raw commands into typed
     ones and top-level declaration of the main Gallina objects *)
@@ -24,11 +23,6 @@ val do_universe : polymorphic -> Id.t Loc.located list -> unit
 val do_constraint : polymorphic ->
   (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
 
-(** {6 Hooks for Pcoq} *)
-
-val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit
-val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit)
-
 (** {6 Definitions/Let} *)
 
 val interp_definition :
@@ -36,10 +30,6 @@ val interp_definition :
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
-val declare_definition : Id.t -> definition_kind ->
-  Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
-    Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
-
 val do_definition : Id.t -> definition_kind -> lident list option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
@@ -91,9 +81,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 *)
@@ -105,8 +95,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} *)
 
@@ -151,7 +141,7 @@ val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
-  lemma_possible_guards -> decl_notation list -> unit
+  Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
@@ -171,6 +161,3 @@ val do_cofixpoint :
 (** Utils *)
 
 val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit
-
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
-  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
new file mode 100644
index 0000000000..d7a4fcca3d
--- /dev/null
+++ b/vernac/declareDef.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Decl_kinds
+open Declare
+open Entries
+open Globnames
+open Impargs
+open Nameops
+
+let warn_definition_not_visible =
+  CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
+    Pp.(fun ident ->
+        strbrk "Section definition " ++
+        pr_id ident ++ strbrk " is not visible from current goals")
+
+let warn_local_declaration =
+  CWarnings.create ~name:"local-declaration" ~category:"scope"
+    Pp.(fun (id,kind) ->
+        pr_id id ++ strbrk " is declared as a local " ++ str kind)
+
+let get_locality id ~kind = function
+| Discharge ->
+  (** If a Let is defined outside a section, then we consider it as a local definition *)
+   warn_local_declaration (id,kind);
+  true
+| Local -> true
+| Global -> false
+
+let declare_global_definition ident ce local k pl imps =
+  let local = get_locality ident ~kind:"definition" local in
+  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+  let gr = ConstRef kn in
+  let () = maybe_declare_manual_implicits false gr imps in
+  let () = Universes.register_universe_binders gr pl in
+  let () = definition_message ident in
+  gr
+
+let declare_definition ident (local, p, k) ce pl imps hook =
+  let fix_exn = Future.fix_exn_of ce.const_entry_body in
+  let r = match local with
+  | Discharge when Lib.sections_are_opened () ->
+    let c = SectionLocalDef ce in
+    let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
+    let () = definition_message ident in
+    let gr = VarRef ident in
+    let () = maybe_declare_manual_implicits false gr imps in
+    let () = if Proof_global.there_are_pending_proofs () then
+	       warn_definition_not_visible ident
+    in
+    gr
+  | Discharge | Local | Global ->
+    declare_global_definition ident ce local k pl imps in
+  Lemmas.call_hook fix_exn hook local r
+
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
+  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
+  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
new file mode 100644
index 0000000000..5dea0ba272
--- /dev/null
+++ b/vernac/declareDef.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Decl_kinds
+open Names
+
+val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
+
+val declare_definition : Id.t -> definition_kind ->
+  Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
+    Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
+
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+  Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 65ade78876..18f93334b1 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -79,12 +79,14 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
 
 let process_inductive (sechyps,abs_ctx) modlist mib =
   let nparams = mib.mind_nparams in
-  let subst, univs = 
-    if mib.mind_polymorphic then 
-      let inst = Univ.UContext.instance mib.mind_universes in
-      let cstrs = Univ.UContext.constraints mib.mind_universes in
-	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
-    else Univ.Instance.empty, mib.mind_universes
+  let subst, univs =
+    match mib.mind_universes with
+    | Monomorphic_ind ctx -> Univ.Instance.empty, ctx
+    | Polymorphic_ind auctx ->
+      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
+    | Cumulative_ind cumi ->
+      let auctx = Univ.ACumulativityInfo.univ_context cumi in
+      Univ.AUContext.instance auctx, Univ.instantiate_univ_context auctx
   in
   let inds =
     Array.map_to_list
@@ -105,6 +107,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
+  let ind_univs =
+    match mib.mind_universes with
+    | Monomorphic_ind _ -> Monomorphic_ind_entry univs
+    | Polymorphic_ind _ -> Polymorphic_ind_entry univs
+    | Cumulative_ind _ ->
+      Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs) in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
@@ -114,7 +122,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_finite = mib.mind_finite;
     mind_entry_params = params';
     mind_entry_inds = inds';
-    mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univs;
+    mind_entry_universes = ind_univs
   }
+
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index 18d1b67766..3845c04a11 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,4 +11,5 @@ open Entries
 open Opaqueproof
 
 val process_inductive :
-  Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
+  -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 6d8dd82ac6..ce91e1a09f 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -889,6 +889,10 @@ let explain_not_match_error = function
   | NoTypeConstraintExpected ->
     strbrk "a definition whose type is constrained can only be subtype " ++
     strbrk "of a definition whose type is itself constrained"
+  | CumulativeStatusExpected b ->
+    let status b = if b then str"cumulative" else str"non-cumulative" in
+      str "a " ++ status b ++ str" declaration was expected, but a " ++ 
+	status (not b) ++ str" declaration was found"
   | PolymorphicStatusExpected b ->
     let status b = if b then str"polymorphic" else str"monomorphic" in
       str "a " ++ status b ++ str" declaration was expected, but a " ++ 
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index f3259f1f3b..65d42b6267 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -148,7 +148,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let id = match idopt with
     | Some id -> id
     | None -> add_suffix mib.mind_packets.(i).mind_typename suff in
-  let const = define mode id c mib.mind_polymorphic ctx in
+  let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in
   declare_scheme kind [|ind,const|];
   const, Safe_typing.add_private
      (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
@@ -166,7 +166,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
       try Int.List.assoc i names
       with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in
   let consts = Array.map2 (fun id cl -> 
-     define mode id cl mib.mind_polymorphic ctx) ids cl in
+     define mode id cl (Declareops.inductive_is_polymorphic mib) ctx) ids cl in
   let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in
   declare_scheme kind schemes;
   consts,
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78e..44d6f37cc6 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,15 +84,8 @@ let _ =
       optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
-let _ = (* compatibility *)
-  declare_bool_option
-    { optdepr  = true;
-      optname  = "automatic declaration of boolean equality";
-      optkey   = ["Equality";"Scheme"];
-      optread  = (fun () -> !eq_flag) ;
-      optwrite = (fun b -> eq_flag := b) }
 
-let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+let is_eq_flag () = !eq_flag
 
 let eq_dec_flag = ref false 
 let _ =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 77e356eb2c..5bf419caf5 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -209,7 +209,7 @@ let compute_proof_name locality = function
         user_err ?loc  (pr_id id ++ str " already exists.");
       id, pl
   | None ->
-      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
+      next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None
 
 let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
   let t_i = norm t_i in
@@ -487,7 +487,7 @@ let save_proof ?proof = function
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
             Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
         | None ->
-            let pftree = Pfedit.get_pftreestate () in
+            let pftree = Proof_global.give_me_the_proof () in
             let id, k, typ = Pfedit.current_proof_statement () in
             let typ = EConstr.Unsafe.to_constr typ in
             let universes = Proof.initial_euctx pftree in
@@ -496,7 +496,7 @@ let save_proof ?proof = function
               Proof_global.return_proof ~allow_partial:true () in
             let sec_vars =
               if not !keep_admitted_vars then None
-              else match  Pfedit.get_used_variables(), pproofs with
+              else match Proof_global.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
               | None, (pproof, _) :: _ -> 
                   let env = Global.env () in
@@ -504,7 +504,7 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-	    let names = Pfedit.get_universe_binders () in
+	    let names = Proof_global.get_universe_binders () in
             let evd = Evd.from_ctx universes in
             let binders, ctx = Evd.universe_context ?names evd in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
@@ -519,7 +519,7 @@ let save_proof ?proof = function
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
-      if Option.is_empty proof then Pfedit.delete_current_proof ();
+      if Option.is_empty proof then Proof_global.discard_current ();
       Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj)))
 
 (* Miscellaneous *)
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index d06b8fd14b..a9c0d99f30 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Decl_kinds
-open Pfedit
 
 type 'a declaration_hook
 val mk_hook :
@@ -21,16 +20,16 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (EConstr.types -> unit) -> unit
 
-val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map ->
-  ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map ->
+  ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
-  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
   (Evd.evar_universe_context option -> unit declaration_hook) -> unit
 
 val start_proof_com :
@@ -40,8 +39,8 @@ val start_proof_com :
 
 val start_proof_with_initialization : 
   goal_kind -> Evd.evar_map ->
-  (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
-  ((Id.t (* name of thm *) * universe_binders option) *
+  (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
+  ((Id.t (* name of thm *) * Proof_global.universe_binders option) *
      (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6dee95bc54..c0acdaf57d 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -22,9 +22,6 @@ open Util
 
 module NamedDecl = Context.Named.Declaration
 
-let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
-let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
-
 let get_fix_exn, stm_get_fix_exn = Hook.make ()
 
 let succfix (depth, fixrels) =
@@ -365,8 +362,8 @@ let get_body obl =
   match obl.obl_body with
   | None -> None
   | Some (DefinedObl c) ->
-    let ctx = Environ.constant_context (Global.env ()) c in
-    let pc = (c, Univ.UContext.instance ctx) in
+    let u = Environ.constant_instance (Global.env ()) c in
+    let pc = (c, u) in
       Some (DefinedObl pc)
   | Some (TermObl c) ->
       Some (TermObl c)
@@ -496,14 +493,12 @@ let declare_definition prg =
   in
   let () = progmap_remove prg in
   let cst =
-    !declare_definition_ref prg.prg_name 
-     prg.prg_kind ce prg.prg_implicits
+    DeclareDef.declare_definition prg.prg_name
+     prg.prg_kind ce [] prg.prg_implicits
      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
   in
   Universes.register_universe_binders cst pl;
   cst
-      
-open Pp
 
 let rec lam_index n t acc =
   match kind_of_term t with
@@ -569,7 +564,7 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
-  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
+  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) [] ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
@@ -947,7 +942,7 @@ let rec solve_obligation prg num tac =
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
   let _ = Pfedit.by !default_tactic in
-  Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
+  Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac
 
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a276f9f9a3..9cbbf6082c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -12,23 +12,12 @@ open Evd
 open Names
 open Pp
 open Globnames
-open Decl_kinds
-
-(** Forward declaration. *)
-val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
-  Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
-
-val declare_definition_ref :
-  (Id.t -> definition_kind ->
-     Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits
-       -> global_reference Lemmas.declaration_hook -> global_reference) ref
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
  * is not available here, so we provide a side channel to get it *)
 val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
 
-
 val check_evars : env -> evar_map -> unit
 
 val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
diff --git a/vernac/record.ml b/vernac/record.ml
index 2400fa6814..7dd70d0133 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -265,10 +265,16 @@ let warn_non_primitive_record =
 let declare_projections indsp ?(kind=StructureComponent) binder_name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let u = Declareops.inductive_instance mib in
+  let u = Declareops.inductive_polymorphic_instance mib in
   let paramdecls = Inductive.inductive_paramdecls (mib, u) in
-  let poly = mib.mind_polymorphic in
-  let ctx = Univ.instantiate_univ_context mib.mind_universes in
+  let poly = Declareops.inductive_is_polymorphic mib in
+  let ctx =
+    match mib.mind_universes with
+    | Monomorphic_ind ctx -> ctx
+    | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+    | Cumulative_ind cumi -> 
+      Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+  in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
   let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
@@ -377,12 +383,18 @@ let structure_signature ctx =
 
 open Typeclasses
 
-let declare_structure finite poly ctx id idbuild paramimpls params arity template 
+let declare_structure finite univs 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
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
+  let poly, ctx =
+    match univs with
+    | Monomorphic_ind_entry ctx -> false, ctx
+    | Polymorphic_ind_entry ctx -> true, ctx
+    | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+  in
   let binder_name = 
     match name with
     | None -> Id.of_string (Unicode.lowercase_first_char (Id.to_string id)) 
@@ -400,11 +412,22 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
       mind_entry_finite = finite;
       mind_entry_inds = [mie_ind];
-      mind_entry_polymorphic = poly;
       mind_entry_private = None;
-      mind_entry_universes = ctx;
+      mind_entry_universes = univs;
     }
   in
+  let mie =
+    if poly then
+      begin
+        let env = Global.env () in
+        let env' = Environ.push_context ctx env in
+        (* let env'' = Environ.push_rel_context params env' in *)
+        let evd = Evd.from_env env' in
+        Inductiveops.infer_inductive_subtyping env' evd mie
+      end
+    else
+       mie
+  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
@@ -423,7 +446,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. *)
@@ -466,7 +489,16 @@ 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 univs =
+         if poly then
+           if cum then
+             Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+           else
+             Polymorphic_ind_entry ctx
+         else
+           Monomorphic_ind_entry ctx
+       in
+       let ind = declare_structure BiFinite univs (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -515,7 +547,7 @@ let add_inductive_class ind =
   let mind, oneind = Global.lookup_inductive ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
-    let inst = Univ.UContext.instance mind.mind_universes in
+    let inst = Declareops.inductive_polymorphic_instance mind in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
@@ -540,7 +572,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
@@ -564,14 +596,24 @@ 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
+      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
+	           (succ (List.length params)) impls) implfs 
+      in
+      let univs =
+        if poly then
+          if cum then
+            Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+          else
+            Polymorphic_ind_entry ctx
+        else
+          Monomorphic_ind_entry ctx
+      in
+      let ind = declare_structure finite univs 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 3fd651db90..aa530fd61a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,7 +26,7 @@ val declare_projections :
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
-  bool (** polymorphic?*) -> Univ.universe_context ->
+  Entries.inductive_universes ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
@@ -38,8 +38,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/search.ml b/vernac/search.ml
index 0ff78f439d..5e56ada8ad 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -85,7 +85,7 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
     let mib = Global.lookup_mind mind in
     let iter_packet i mip =
       let ind = (mind, i) in
-      let u = Declareops.inductive_instance mib in
+      let u = Declareops.inductive_polymorphic_instance mib in
       let i = (ind, u) in
       let typ = Inductiveops.type_of_inductive env i in
       let () = fn (IndRef ind) env typ in
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index d631fae8a8..f74073e1f7 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -8,6 +8,7 @@ Metasyntax
 Auto_ind_decl
 Search
 Indschemes
+DeclareDef
 Obligations
 Command
 Classes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..acd2185365 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -15,7 +15,6 @@ open Flags
 open Names
 open Nameops
 open Term
-open Pfedit
 open Tacmach
 open Constrintern
 open Prettyp
@@ -61,35 +60,25 @@ let show_proof () =
   let pprf = Proof.partial_proof p in
   Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
 
-let show_node () =
-  (* spiwack: I'm have little clue what this function used to do. I deactivated it, 
-      could, possibly, be cleaned away. (Feb. 2010) *)
-  ()
-
-let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.")
-
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
-  let pfts = get_pftreestate () in
+  let pfts = Proof_global.give_me_the_proof () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma))
 
 let show_universes () =
-  let pfts = get_pftreestate () in
+  let pfts = Proof_global.give_me_the_proof () in
   let gls = Proof.V82.subgoals pfts in
   let sigma = gls.Evd.sigma in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
     Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
     Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
 
-(* Spiwack: proof tree is currently not working *)
-let show_prooftree () = ()
-
 (* Simulate the Intro(s) tactic *)
 let show_intro all =
   let open EConstr in
-  let pf = get_pftreestate() in
+  let pf = Proof_global.give_me_the_proof() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
   if not (List.is_empty gls) then begin
     let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
@@ -501,17 +490,13 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
  		Some (snd (Hook.get f_interp_redexp env evc r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
-let vernac_start_proof locality p kind l lettop =
+let vernac_start_proof locality p kind l =
   let local = enforce_locality_exp locality None in
   if Dumpglob.dump () then
     List.iter (fun (id, _) ->
       match id with
 	| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
 	| None -> ()) l;
-  if not(refining ()) then
-    if lettop then
-      user_err ~hdr:"Vernacentries.StartProof"
-	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (local, p, Proof kind) l no_hook
 
 let vernac_end_proof ?proof = function
@@ -521,7 +506,7 @@ let vernac_end_proof ?proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-  let status = by (Tactics.exact_proof c) in
+  let status = Pfedit.by (Tactics.exact_proof c) in
   save_proof (Vernacexpr.(Proved(Opaque None,None)));
   if not status then Feedback.feedback Feedback.AddedAxiom
 
@@ -537,7 +522,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) ->
@@ -548,13 +533,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
@@ -570,14 +555,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 _, _), _ :: _ ] ->
@@ -591,7 +576,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
@@ -639,8 +624,7 @@ let vernac_constraint loc poly l =
 (* Modules            *)
 
 let vernac_import export refl =
-  Library.import_module export (List.map qualid_of_reference refl);
-  Lib.add_frozen_state ()
+  Library.import_module export (List.map qualid_of_reference refl)
 
 let vernac_declare_module export (loc, id) binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
@@ -667,7 +651,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
     user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
-       check_no_pending_proofs ();
+       Proof_global.check_no_pending_proof ();
        let binders_ast,argsexport =
         List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -713,7 +697,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 
   match mty_ast_l with
     | [] ->
-       check_no_pending_proofs ();
+       Proof_global.check_no_pending_proof ();
        let binders_ast,argsexport =
 	 List.fold_right
          (fun (export,idl,ty) (args,argsexport) ->
@@ -761,7 +745,7 @@ let vernac_include l =
 (* Sections *)
 
 let vernac_begin_section (_, id as lid) =
-  check_no_pending_proofs ();
+  Proof_global.check_no_pending_proof ();
   Dumpglob.dump_definition lid true "sec";
   Lib.open_section id
 
@@ -775,7 +759,7 @@ let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set
 (* Dispatcher of the "End" command *)
 
 let vernac_end_segment (_,id as lid) =
-  check_no_pending_proofs ();
+  Proof_global.check_no_pending_proof ();
   match Lib.find_opening_node id with
   | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid
   | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid
@@ -855,14 +839,14 @@ let focus_command_cond = Proof.no_cond command_focus
      there are no more goals to solve. It cannot be a tactic since
      all tactics fail if there are no further goals to prove. *)
 
-let vernac_solve_existential = instantiate_nth_evar_com
+let vernac_solve_existential = Pfedit.instantiate_nth_evar_com
 
 let vernac_set_end_tac tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
-  if not (refining ()) then
+  if not (Proof_global.there_are_pending_proofs ()) then
     user_err Pp.(str "Unknown command of the non proof-editing mode.");
-  set_end_tac tac
+  Proof_global.set_endline_tactic tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables e =
@@ -877,13 +861,13 @@ let vernac_set_used_variables e =
       user_err ~hdr:"vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
-  let _, to_clear = set_used_variables l in
+  let _, to_clear = Proof_global.set_used_variables l in
   let to_clear = List.map snd to_clear in
   Proof_global.with_current_proof begin fun _ p ->
     if List.is_empty to_clear then (p, ())
     else
       let tac = Tactics.clear to_clear in
-      fst (solve SelectAll None tac p), ()
+      fst (Pfedit.solve SelectAll None tac p), ()
   end
 
 (*****************************)
@@ -927,12 +911,12 @@ let vernac_chdir = function
 (* State management *)
 
 let vernac_write_state file =
-  Pfedit.delete_all_proofs ();
+  Proof_global.discard_all ();
   let file = CUnix.make_suffix file ".coq" in
   States.extern_state file
 
 let vernac_restore_state file =
-  Pfedit.delete_all_proofs ();
+  Proof_global.discard_all ();
   let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
   States.intern_state file
 
@@ -1298,7 +1282,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic introduction of variables";
       optkey   = ["Automatic";"Introduction"];
       optread  = Flags.is_auto_intros;
@@ -1377,6 +1361,14 @@ let _ =
       optwrite = Flags.make_universe_polymorphism }
 
 let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "inductive cumulativity";
+      optkey   = ["Inductive"; "Cumulativity"];
+      optread  = Flags.is_inductive_cumulativity;
+      optwrite = Flags.make_inductive_cumulativity }
+
+let _ =
   declare_int_option
     { optdepr  = false;
       optname  = "the level of inlining during functor application";
@@ -1394,17 +1386,6 @@ let _ =
       optread  = (fun () -> !CClosure.share);
       optwrite = (fun b -> CClosure.share := b) }
 
-(* No more undo limit in the new proof engine.
-   The command still exists for compatibility (e.g. with ProofGeneral) *)
-
-let _ =
-  declare_int_option
-    { optdepr  = true;
-      optname  = "the undo limit (OBSOLETE)";
-      optkey   = ["Undo"];
-      optread  = (fun _ -> None);
-      optwrite = (fun _ -> ()) }
-
 let _ =
   declare_bool_option
     { optdepr  = false;
@@ -1526,7 +1507,7 @@ let vernac_print_option key =
   with Not_found -> error_undeclared_key key
 
 let get_current_context_of_args = function
-  | Some n -> get_goal_context n
+  | Some n -> Pfedit.get_goal_context n
   | None -> get_current_context ()
 
 let query_command_selector ?loc = function
@@ -1588,7 +1569,7 @@ let vernac_global_check c =
 
 
 let get_nth_goal n =
-  let pf = get_pftreestate() in
+  let pf = Proof_global.give_me_the_proof() in
   let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
   let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
   gl
@@ -1777,7 +1758,7 @@ let vernac_locate = let open Feedback in function
   | LocateFile f -> msg_notice (locate_file f)
 
 let vernac_register id r =
- if Pfedit.refining () then
+ if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   let kn = Constrintern.global_reference (snd id) in
   if not (isConstRef kn) then
@@ -1844,24 +1825,16 @@ let vernac_show = let open Feedback in function
       | GoalUid id -> pr_goal_by_uid id
     in
     msg_notice info
-  | ShowGoalImplicitly None ->
-      Constrextern.with_implicits msg_notice (pr_open_subgoals ())
-  | ShowGoalImplicitly (Some n) ->
-      Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n)
   | ShowProof -> show_proof ()
-  | ShowNode -> show_node ()
   | ShowExistentials -> show_top_evars ()
   | ShowUniverses -> show_universes ()
-  | ShowTree -> show_prooftree ()
   | ShowProofNames ->
-      msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names()))
+      msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
-  | ShowThesis -> show_thesis ()
-
 
 let vernac_check_guard () =
-  let pts = get_pftreestate () in
+  let pts = Proof_global.give_me_the_proof () in
   let pfterm = List.hd (Proof.partial_proof pts) in
   let message =
     try
@@ -1960,11 +1933,11 @@ let interp ?proof ?loc locality poly c =
 
   (* Gallina *)
   | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d
-  | VernacStartTheoremProof (k,l,top) -> vernac_start_proof locality poly k l top
+  | VernacStartTheoremProof (k,l) -> vernac_start_proof locality poly k l
   | 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
@@ -2048,7 +2021,7 @@ let interp ?proof ?loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
-  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)]
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()