From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
---
 vernac/command.ml       |  4 ++--
 vernac/command.mli      |  3 +--
 vernac/lemmas.ml        | 10 +++++-----
 vernac/lemmas.mli       | 17 ++++++++---------
 vernac/obligations.ml   |  2 +-
 vernac/vernacentries.ml | 43 +++++++++++++++++++++----------------------
 6 files changed, 38 insertions(+), 41 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index b1425d7034..998e7803e1 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -187,7 +187,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
     let () = definition_message ident in
     let gr = VarRef ident in
     let () = maybe_declare_manual_implicits false gr imps in
-    let () = if Pfedit.refining () then
+    let () = if Proof_global.there_are_pending_proofs () then
 	       warn_definition_not_visible ident
     in
     gr
@@ -233,7 +233,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
diff --git a/vernac/command.mli b/vernac/command.mli
index 9bbc2fdac1..2a52d9bcb5 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 *)
@@ -151,7 +150,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 * 
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..e03e9b8039 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -947,7 +947,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/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..5d1def7a4b 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
@@ -70,13 +69,13 @@ 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
@@ -89,7 +88,7 @@ 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
@@ -508,7 +507,7 @@ let vernac_start_proof locality p kind l lettop =
       match id with
 	| Some (lid,_) -> Dumpglob.dump_definition lid false "prf"
 	| None -> ()) l;
-  if not(refining ()) then
+  if not(Proof_global.there_are_pending_proofs ()) then
     if lettop then
       user_err ~hdr:"Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
@@ -521,7 +520,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
 
@@ -667,7 +666,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 +712,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 +760,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 +774,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 +854,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 +876,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 +926,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
 
@@ -1526,7 +1525,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 +1587,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 +1776,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
@@ -1854,14 +1853,14 @@ let vernac_show = let open Feedback in function
   | 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
-- 
cgit v1.2.3


From 2253d2eb4f892f932332358be8537fdb5552ef87 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:08:12 +0200
Subject: Remove Show Implicit Arguments command.

The command has been broken for 15 years. It is basically dead code.
Its former behavior can be mimicked with Set Printing Implicit. Show.
---
 vernac/vernacentries.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..c0272f2108 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1844,10 +1844,6 @@ 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 ()
-- 
cgit v1.2.3


From 6cd14bf253f681d0465f8dce1d84a54a4f104d9c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:22:38 +0200
Subject: Remove non-working Show Tree and Show Node commands.

---
 vernac/vernacentries.ml | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c0272f2108..e0eeaf563b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -61,11 +61,6 @@ 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 () =
@@ -83,9 +78,6 @@ let show_universes () =
     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
@@ -1845,10 +1837,8 @@ let vernac_show = let open Feedback in function
     in
     msg_notice info
   | 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()))
   | ShowIntros all -> show_intro all
-- 
cgit v1.2.3


From 3813ba5229cf42597cd30a08e842e0832e5253cb Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 12 Jun 2017 11:25:26 +0200
Subject: Remove Show Thesis command which was never implemented.

---
 vernac/vernacentries.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e0eeaf563b..6830a5da1a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -61,8 +61,6 @@ 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_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
@@ -1843,8 +1841,6 @@ let vernac_show = let open Feedback in function
       msg_notice (pr_sequence pr_id (Pfedit.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
-- 
cgit v1.2.3


From 63896b2443e71e47c016fc9d0709cc22cf24f288 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 12:37:55 +0200
Subject: [lib] Remove obsolete state-management function add_frozen_state

AFAICS this function predates modern state-handling; nowadays
summaries are stored by the STM and nobody were using this
information.
---
 vernac/vernacentries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..338e7c06e3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -639,8 +639,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)
-- 
cgit v1.2.3


From 6332f43dfee3efc890c5f8fdc1b5b54942c16307 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 May 2017 09:55:40 +0200
Subject: Explicit the unsafe flag of all calls to Refine.refine.

---
 vernac/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8e6a0f6a72..3cd0a8de85 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -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 ~unsafe:true (fun evm -> (evm,EConstr.of_constr (Option.get term)));
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]
-- 
cgit v1.2.3


From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Jun 2017 10:33:56 +0200
Subject: Dualize the unsafe flag of refine into typecheck and make it
 mandatory.

---
 vernac/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3cd0a8de85..aba61146c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -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 ~unsafe:true (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;
                     ]
-- 
cgit v1.2.3


From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:08:14 +0100
Subject: Remove support for Coq 8.2.

---
 vernac/indschemes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78e..e90c259263 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -92,7 +92,7 @@ let _ = (* compatibility *)
       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 _ =
-- 
cgit v1.2.3


From 376da97be60957b25e59afb5791fae665127b17b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:48:14 +0100
Subject: Remove options deprecated since 8.4.

---
 vernac/indschemes.ml    |  7 -------
 vernac/vernacentries.ml | 11 -----------
 2 files changed, 18 deletions(-)

(limited to 'vernac')

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e90c259263..44d6f37cc6 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,13 +84,6 @@ 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
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..9978848ff3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1394,17 +1394,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;
-- 
cgit v1.2.3


From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:51:32 +0100
Subject: Deprecate options that were introduced for compatibility with 8.2.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9978848ff3..ba1da655a8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1298,7 +1298,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;
-- 
cgit v1.2.3


From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Tue, 28 Mar 2017 19:24:02 +0200
Subject: Extend definition of inductives to include subtyping info

---
 vernac/command.ml   | 2 +-
 vernac/discharge.ml | 9 ++++++++-
 vernac/record.ml    | 4 ++--
 vernac/record.mli   | 3 ++-
 4 files changed, 13 insertions(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 998e7803e1..5f95a42a37 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = uctx;
+    mind_entry_universes = (uctx, Univ.UContext.empty);
   },
     pl, impls
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 65ade78876..9c70eb97ef 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -86,6 +86,13 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
 	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
     else Univ.Instance.empty, mib.mind_universes
   in
+  let substsbt, univssbt = 
+    if mib.mind_polymorphic then 
+      let inst = Univ.UContext.instance mib.mind_subtyping in
+      let cstrs = Univ.UContext.constraints mib.mind_subtyping in
+	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
+    else Univ.Instance.empty, Univ.UContext.empty
+  in
   let inds =
     Array.map_to_list
       (fun mip ->
@@ -116,5 +123,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univs;
+    mind_entry_universes = (univs, univssbt);
   }
diff --git a/vernac/record.ml b/vernac/record.ml
index 2400fa6814..5c76bb4b2d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
@@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite poly ctx idstruc
+	let ind = declare_structure finite poly (ctx, Univ.UContext.empty) 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..a380b041a4 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?*) -> Univ.universe_context ->
+  bool (** polymorphic?*) ->
+  (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
-- 
cgit v1.2.3


From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sat, 1 Apr 2017 17:35:39 +0200
Subject: Using UInfoInd for universes in inductive types

It stores both universe constraints and subtyping information for
blocks of inductive declarations.

At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
---
 vernac/command.ml   |  2 +-
 vernac/discharge.ml | 16 +++++-----------
 vernac/record.ml    |  8 ++++----
 vernac/record.mli   |  2 +-
 4 files changed, 11 insertions(+), 17 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 5f95a42a37..b76c2247b3 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -656,7 +656,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = (uctx, Univ.UContext.empty);
+    mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx;
   },
     pl, impls
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 9c70eb97ef..91e126ef1d 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -81,17 +81,10 @@ 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
+      let inst = Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) in
+      let cstrs = Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes) in
 	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
-    else Univ.Instance.empty, mib.mind_universes
-  in
-  let substsbt, univssbt = 
-    if mib.mind_polymorphic then 
-      let inst = Univ.UContext.instance mib.mind_subtyping in
-      let cstrs = Univ.UContext.constraints mib.mind_subtyping in
-	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
-    else Univ.Instance.empty, Univ.UContext.empty
+    else Univ.Instance.empty, (Univ.UInfoInd.univ_context mib.mind_universes)
   in
   let inds =
     Array.map_to_list
@@ -112,6 +105,7 @@ 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 univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in (* Here we must re-infer subtyping constraints. For now we just revert to trivial subtyping. *)
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None
@@ -123,5 +117,5 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = (univs, univssbt);
+    mind_entry_universes = univ_info_ind
   }
diff --git a/vernac/record.ml b/vernac/record.ml
index 5c76bb4b2d..64f5e81d41 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -268,7 +268,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let u = Declareops.inductive_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 ctx = Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes) 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
@@ -466,7 +466,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite poly (ctx, Univ.UContext.empty) (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite 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
@@ -515,7 +515,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 = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in
     let ty = Inductive.type_of_inductive
       (push_rel_context ctx (Global.env ()))
       ((mind,oneind),inst)
@@ -571,7 +571,7 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite poly (ctx, Univ.UContext.empty) idstruc
+	let ind = declare_structure finite 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 a380b041a4..ec5d2cf83d 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -27,7 +27,7 @@ val declare_projections :
 val declare_structure :
   Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) ->
-  (Univ.universe_context * Univ.universe_context) (** universe and subtyping constraints *) ->
+  Univ.universe_info_ind (** universe and subtyping constraints *) ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
-- 
cgit v1.2.3


From d83a4a93202c91095c5528fe4b54c83737e5a151 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Tue, 4 Apr 2017 19:44:31 +0200
Subject: Add subtyping inference for inductive types

---
 vernac/command.ml | 54 +++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 53 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index b76c2247b3..b23eb9e6bf 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -573,6 +573,32 @@ let check_param = function
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
 
+let infer_inductive_subtyping_arity_constructor
+  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
+  let update_contexts (env, evd, csts) csts' =
+    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
+  in
+  let basic_check (env, evd, csts) tp =
+    let csts' =
+      Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
+    in update_contexts (env, evd, csts) csts'
+  in
+  let infer_typ typ ctxs =
+   match typ with
+     | LocalAssum (_, typ') ->
+       begin
+         try
+           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
+         with Reduction.NotConvertible -> 
+           anomaly ~label:"inference of record/inductive subtyping relation failed"
+             (Pp.str "Can't infer subtyping for record/inductive type")
+       end
+     | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = Reduction.dest_prod env arcn in
+  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
+  if not is_arity then basic_check last_contexts codom else last_contexts
+
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
@@ -649,6 +675,32 @@ 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 ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in
+  let uinfind =
+    let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
+    let dosubst = subst_univs_level_constr sbsubst in
+    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
+    let env' = Environ.push_context uctx env_ar_params in
+    let env' = Environ.push_context uctx_other env' in
+    let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
+    let (_, _, subtyp_constraints) =
+      List.fold_left
+       (fun ctxs indentry ->
+          let ctxs' = infer_inductive_subtyping_arity_constructor
+                        ctxs dosubst indentry.mind_entry_arity true
+          in
+          List.fold_left
+           (fun ctxs cons ->
+              infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
+           ctxs' indentry.mind_entry_lc
+       ) (env', evd', Univ.Constraint.empty) entries
+    in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
+         Univ.UContext.make
+           (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
+             subtyp_constraints))
+  in
   (* Build the mutual inductive entry *)
   { mind_entry_params = List.map prepare_param ctx_params;
     mind_entry_record = None;
@@ -656,7 +708,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = Universes.univ_inf_ind_from_universe_context uctx;
+    mind_entry_universes = uinfind;
   },
     pl, impls
 
-- 
cgit v1.2.3


From bef2e53ae2286d0a7c61697f7a7a71bfdc0a3c99 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 5 Apr 2017 14:49:13 +0200
Subject: Subtyping inference for inductoves and records

Also reinferred after sections discharge
---
 vernac/command.ml   | 70 ++++++++---------------------------------------------
 vernac/discharge.ml | 31 +++++++++++++++++-------
 vernac/record.ml    | 12 +++++++++
 3 files changed, 44 insertions(+), 69 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index b23eb9e6bf..35b75370e4 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -573,32 +573,6 @@ let check_param = function
 | CLocalAssum (nas, Generalized _, _) -> ()
 | CLocalPattern _ -> assert false
 
-let infer_inductive_subtyping_arity_constructor
-  (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity =
-  let update_contexts (env, evd, csts) csts' =
-    (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
-  in
-  let basic_check (env, evd, csts) tp =
-    let csts' =
-      Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
-    in update_contexts (env, evd, csts) csts'
-  in
-  let infer_typ typ ctxs =
-   match typ with
-     | LocalAssum (_, typ') ->
-       begin
-         try
-           let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
-         with Reduction.NotConvertible -> 
-           anomaly ~label:"inference of record/inductive subtyping relation failed"
-             (Pp.str "Can't infer subtyping for record/inductive type")
-       end
-     | _ -> anomaly (Pp.str "")
-  in
-  let typs, codom = Reduction.dest_prod env arcn in
-  let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
-  if not is_arity then basic_check last_contexts codom else last_contexts
-
 let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
@@ -676,41 +650,17 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
   let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx in
-  let uinfind =
-    let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in
-    let dosubst = subst_univs_level_constr sbsubst in
-    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
-    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env' = Environ.push_context uctx env_ar_params in
-    let env' = Environ.push_context uctx_other env' in
-    let evd' = Evd.merge_universe_context evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) in
-    let (_, _, subtyp_constraints) =
-      List.fold_left
-       (fun ctxs indentry ->
-          let ctxs' = infer_inductive_subtyping_arity_constructor
-                        ctxs dosubst indentry.mind_entry_arity true
-          in
-          List.fold_left
-           (fun ctxs cons ->
-              infer_inductive_subtyping_arity_constructor ctxs dosubst cons false)
-           ctxs' indentry.mind_entry_lc
-       ) (env', evd', Univ.Constraint.empty) entries
-    in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind,
-         Univ.UContext.make
-           (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind),
-             subtyp_constraints))
-  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 = uinfind;
-  },
-    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_polymorphic = poly;
+      mind_entry_private = if prv then Some false else None;
+      mind_entry_universes = ground_uinfind;
+    }
+  in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 91e126ef1d..21ffa4cbff 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -105,17 +105,30 @@ 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 univ_info_ind = Universes.univ_inf_ind_from_universe_context univs in (* Here we must re-infer subtyping constraints. For now we just revert to trivial subtyping. *)
+  let univ_info_ind = 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
     | None -> None
   in
-  { mind_entry_record = record;
-    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 = univ_info_ind
-  }
+  let mind_ent =
+    { mind_entry_record = record;
+      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 = univ_info_ind
+    }
+  in
+  if mib.mind_polymorphic then
+    begin
+      let env = Global.env () in
+      let env' = Environ.push_context univs env in
+      let (env'', typed_params) = Typeops.infer_local_decls env' params' in
+      let evd = Evd.from_env env'' in
+      Inductiveops.infer_inductive_subtyping env'' evd mind_ent
+    end
+  else
+    mind_ent
+
diff --git a/vernac/record.ml b/vernac/record.ml
index 64f5e81d41..84312594d5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -405,6 +405,18 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_universes = ctx;
     }
   in
+  let mie =
+    if poly then
+      begin
+        let env = Global.env () in
+        let env' = Environ.push_context (Univ.UInfoInd.univ_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
-- 
cgit v1.2.3


From c07215582ab75faeea864827b153eed80a28527a Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 6 Apr 2017 19:03:24 +0200
Subject: Change the place of inference after sect discharge

---
 vernac/command.ml   |  5 ++++-
 vernac/discharge.ml | 28 ++++++++--------------------
 2 files changed, 12 insertions(+), 21 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 35b75370e4..2d4f051345 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -660,7 +660,10 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
       mind_entry_private = if prv then Some false else None;
       mind_entry_universes = ground_uinfind;
     }
-  in (Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent), pl, impls
+  in
+  (if poly then
+      Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent
+   else mind_ent), pl, impls
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 21ffa4cbff..c7a741c13f 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -111,24 +111,12 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     | Some None -> Some None
     | None -> None
   in
-  let mind_ent =
-    { mind_entry_record = record;
-      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 = univ_info_ind
-    }
-  in
-  if mib.mind_polymorphic then
-    begin
-      let env = Global.env () in
-      let env' = Environ.push_context univs env in
-      let (env'', typed_params) = Typeops.infer_local_decls env' params' in
-      let evd = Evd.from_env env'' in
-      Inductiveops.infer_inductive_subtyping env'' evd mind_ent
-    end
-  else
-    mind_ent
+  { mind_entry_record = record;
+    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 = univ_info_ind
+  }
 
-- 
cgit v1.2.3


From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sun, 21 May 2017 14:46:30 +0200
Subject: Squashed commit of the following:

Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.

This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!

commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon Apr 24 17:14:21 2017 +0200

    Revert STL to monomorphic

commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon Apr 24 17:02:42 2017 +0200

    Try unifying universes before apply subtyping

commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany <amintimany@gmail.com>
Date:   Sun Apr 23 13:49:04 2017 +0200

    Compile more of STL with universe polymorphism

commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany <amintimany@gmail.com>
Date:   Tue Apr 18 21:26:45 2017 +0200

    Made more progress on compiling the standard library

commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany <amintimany@gmail.com>
Date:   Sun Apr 16 22:55:19 2017 +0200

    Make more number theoretic modules monomorphic

commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany <amintimany@gmail.com>
Date:   Fri Apr 14 16:11:48 2017 +0200

    WIP more of standard library compiles

    Also: Matthieu fixed a bug in rewrite system which was faulty when
    introducing new morphisms (Add Morphism) command.

commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany <amintimany@gmail.com>
Date:   Fri Apr 14 11:39:21 2017 +0200

    WIP: more of the standard library compiles

    We have implemented convertibility of constructors up-to mutual
    subtyping of their corresponding inductive types. This is similar to
    the behavior of template polymorphism.

commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany <amintimany@gmail.com>
Date:   Wed Apr 12 19:02:39 2017 +0200

    WIP: trying to get the standard library compile with universe polymorphism

    We are trying to prune universes after section ends. Sections add a
    load of universes that are not appearing in the body, type or the
    constraints.
---
 vernac/classes.ml | 10 ++++++----
 vernac/command.ml | 12 ++++++------
 2 files changed, 12 insertions(+), 10 deletions(-)

(limited to 'vernac')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index aba61146c7..007b70bc0f 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
@@ -420,6 +420,8 @@ let context poly l =
         let _ = Command.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 2d4f051345..116a7aee16 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,
@@ -329,7 +329,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
@@ -1213,7 +1213,7 @@ 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
@@ -1245,7 +1245,7 @@ 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
-- 
cgit v1.2.3


From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 26 Apr 2017 15:24:35 +0200
Subject: Fix bugs

---
 vernac/command.ml | 2 +-
 vernac/record.ml  | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 116a7aee16..6c59976232 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -662,7 +662,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     }
   in
   (if poly then
-      Inductiveops.infer_inductive_subtyping env_ar_params evd mind_ent
+      Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
    else mind_ent), pl, impls
 
 (* Very syntactical equality *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 84312594d5..093a31c194 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -410,9 +410,9 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       begin
         let env = Global.env () in
         let env' = Environ.push_context (Univ.UInfoInd.univ_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
+        (* 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
-- 
cgit v1.2.3


From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

---
 vernac/command.ml       |  7 ++++---
 vernac/command.mli      | 10 +++++-----
 vernac/discharge.ml     |  1 +
 vernac/record.ml        | 13 +++++++------
 vernac/record.mli       |  7 ++++---
 vernac/vernacentries.ml | 28 +++++++++++++++++++++-------
 6 files changed, 42 insertions(+), 24 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 6c59976232..2345cb4c51 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 2a52d9bcb5..a636bc03c5 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 c7a741c13f..738e27f635 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 093a31c194..8a83dceeff 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 ec5d2cf83d..c43d833b0b 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 d0f9c7de74..f130708c40 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
@@ -1364,6 +1364,14 @@ let _ =
       optread  = Flags.is_universe_polymorphism;
       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;
@@ -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). *)
 
-- 
cgit v1.2.3


From 9903b47cdccc2fe98a905ab085cb24ca36de1aed Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 28 Apr 2017 11:12:26 +0200
Subject: Disable debug printing

Fix a mistake in record declaration
---
 vernac/record.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index 8a83dceeff..b95131b724 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -584,7 +584,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	let implfs = List.map
 	  (fun impls -> implpars @ Impargs.lift_implicits
 	    (succ (List.length params)) impls) implfs in
-	let ind = declare_structure Finite cum 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
-- 
cgit v1.2.3


From d6898781f9cd52ac36a4891d7b169ddab7b8af50 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Tue, 2 May 2017 19:53:05 +0200
Subject: Correct coqchk reduction

---
 vernac/vernacentries.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f130708c40..580c81a0bd 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1368,9 +1368,9 @@ let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "inductive cumulativity";
-      optkey   = ["Inductive"; "Cumulativity"];
-      optread  = Flags.is_universe_polymorphism;
-      optwrite = Flags.make_universe_polymorphism }
+      optkey   = ["Ind"; "Cumulativity"];
+      optread  = Flags.is_inductive_cumulativity;
+      optwrite = Flags.make_inductive_cumulativity }
 
 let _ =
   declare_int_option
-- 
cgit v1.2.3


From 7b323421ba558011c304a686c4cd368e1ff39440 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 5 May 2017 13:33:18 +0200
Subject: Change the option to Set Inductive Cumulativity

This requires to change the status of Inductive (we have also changed
CoInductive and Variant) from keyword to identifier.
---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 580c81a0bd..957911e1e5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1368,7 +1368,7 @@ let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "inductive cumulativity";
-      optkey   = ["Ind"; "Cumulativity"];
+      optkey   = ["Inductive"; "Cumulativity"];
       optread  = Flags.is_inductive_cumulativity;
       optwrite = Flags.make_inductive_cumulativity }
 
-- 
cgit v1.2.3


From 249a1910a2474216b7f98491afafc6019a04c894 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 23:46:23 +0200
Subject: Remove Warnings: unused value ...

---
 vernac/vernacentries.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 957911e1e5..21f053fb9b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2091,12 +2091,6 @@ 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). *)
 
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 vernac/command.ml     | 17 ++++++++++------
 vernac/discharge.ml   | 25 +++++++++++++----------
 vernac/discharge.mli  |  3 ++-
 vernac/himsg.ml       |  4 ++++
 vernac/ind_tables.ml  |  4 ++--
 vernac/obligations.ml |  4 ++--
 vernac/record.ml      | 55 +++++++++++++++++++++++++++++++++++++++------------
 vernac/record.mli     |  4 +---
 vernac/search.ml      |  2 +-
 9 files changed, 80 insertions(+), 38 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 2345cb4c51..4064773561 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -649,20 +649,25 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
   in
-  let ground_uinfind = Universes.univ_inf_ind_from_universe_context uctx 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 *)
-  let mind_ent = 
+  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_polymorphic = poly;
-      mind_entry_cumulative = cum;
       mind_entry_private = if prv then Some false else None;
-      mind_entry_universes = ground_uinfind;
+      mind_entry_universes = univs;
     }
   in
-  (if poly then
+  (if poly && cum then
       Inductiveops.infer_inductive_subtyping env_ar evd mind_ent
    else mind_ent), pl, impls
 
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 738e27f635..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 (Univ.UInfoInd.univ_context mib.mind_universes) in
-      let cstrs = Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes) in
-	inst, Univ.UContext.make (inst, Univ.subst_instance_constraints inst cstrs)
-    else Univ.Instance.empty, (Univ.UInfoInd.univ_context 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,7 +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 univ_info_ind = Universes.univ_inf_ind_from_universe_context 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
@@ -115,9 +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_cumulative = mib.mind_cumulative;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univ_info_ind
+    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/obligations.ml b/vernac/obligations.ml
index e03e9b8039..135e4c63ab 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -365,8 +365,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)
diff --git a/vernac/record.ml b/vernac/record.ml
index b95131b724..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 (Univ.UInfoInd.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 cum 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,17 +412,15 @@ let declare_structure finite cum poly ctx id idbuild paramimpls params arity tem
       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_cumulative = cum;
       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 (Univ.UInfoInd.univ_context ctx) 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
@@ -479,7 +489,16 @@ let declare_class finite def cum poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite cum poly (Universes.univ_inf_ind_from_universe_context 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
@@ -528,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 (Univ.UInfoInd.univ_context 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)
@@ -581,10 +600,20 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
 	  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 cum poly (Universes.univ_inf_ind_from_universe_context 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 c43d833b0b..aa530fd61a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,9 +26,7 @@ val declare_projections :
 
 val declare_structure :
   Decl_kinds.recursivity_kind ->
-  Decl_kinds.cumulative_inductive_flag ->
-  Decl_kinds.polymorphic ->
-  Univ.universe_info_ind (** universe and subtyping constraints *) ->
+  Entries.inductive_universes ->
   Id.t -> Id.t ->
   manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
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
-- 
cgit v1.2.3


From 21f8312738f324d1c55e4ed7c451b642c9da70e6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:40:29 +0200
Subject: [vernac] Remove unused hooks.

These hooks are not used (leftovers?) and IMHO they should not be.
---
 vernac/command.ml  | 5 -----
 vernac/command.mli | 5 -----
 2 files changed, 10 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 4064773561..68fa8ab888 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -167,10 +167,6 @@ let declare_global_definition ident ce local k pl imps =
   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 ->
@@ -179,7 +175,6 @@ let warn_definition_not_visible =
 
 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
diff --git a/vernac/command.mli b/vernac/command.mli
index a636bc03c5..f7d90ce607 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -23,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 :
-- 
cgit v1.2.3


From ec8523065abfb68aff9bd3664869224419885385 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:54:07 +0200
Subject: [vernac] Remove forward hooks from Obligations.

This was (once again) a spurious inter-dependency, that we solve by
introducing a new module with the proper functionality. This helps in
cleaning up the code. Note that no code was changed, other than
removing the setting of the references.
---
 vernac/classes.ml      |  2 +-
 vernac/command.ml      | 63 ++++---------------------------------------------
 vernac/command.mli     |  7 ------
 vernac/declareDef.ml   | 64 ++++++++++++++++++++++++++++++++++++++++++++++++++
 vernac/declareDef.mli  | 19 +++++++++++++++
 vernac/obligations.ml  | 11 +++------
 vernac/obligations.mli | 11 ---------
 vernac/vernac.mllib    |  1 +
 8 files changed, 92 insertions(+), 86 deletions(-)
 create mode 100644 vernac/declareDef.ml
 create mode 100644 vernac/declareDef.mli

(limited to 'vernac')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 007b70bc0f..2e8ebb8531 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -417,7 +417,7 @@ 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
 	status && nstatus
diff --git a/vernac/command.ml b/vernac/command.ml
index 68fa8ab888..fd49e53243 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -145,54 +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 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 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 _ = 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
@@ -215,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)))
 
@@ -238,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())
@@ -871,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
@@ -1221,7 +1166,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     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;
@@ -1252,7 +1197,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     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 f7d90ce607..1887885de9 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -30,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
@@ -165,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/obligations.ml b/vernac/obligations.ml
index 135e4c63ab..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) =
@@ -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;
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/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
-- 
cgit v1.2.3


From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 21 Jun 2017 15:12:21 +0200
Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof`

`VernacStartTheoremProof` contained a stale bool parameter from 15
years ago, which is unused today.
---
 vernac/vernacentries.ml | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 21f053fb9b..acd2185365 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -490,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(Proof_global.there_are_pending_proofs ()) 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
@@ -1937,7 +1933,7 @@ 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
@@ -2025,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 ()
-- 
cgit v1.2.3