From 1a43fda0dc9bb8d100808426980446353f8f1ae3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 11:21:23 +0200
Subject: Removing internal support for accepting "{struct x}" and co in
 "Theorem with".

There were actually no syntax for it, and I'm still unsure what good
syntax to give to it, even more that it would be useful to have one.
---
 vernac/lemmas.ml        | 25 ++++---------------------
 vernac/vernacentries.ml |  4 ++--
 2 files changed, 6 insertions(+), 23 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 409676276a..e7d1919ce0 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -88,25 +88,9 @@ let adjust_guardness_conditions const = function
 
 let find_mutually_recursive_statements thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls,annot)) ->
+    let inds = List.map (fun (id,(t,impls)) ->
       let (hyps,ccl) = decompose_prod_assum t in
       let x = (id,(t,impls)) in
-      match annot with
-      (* Explicit fixpoint decreasing argument is given *)
-      | Some (Some (_,id),CStructRec) ->
-          let i,b,typ = lookup_rel_id id hyps in
-          (match kind_of_term t with
-          | Ind ((kn,_ as ind), u) when
-              let mind = Global.lookup_mind kn in
-              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
-              [ind,x,i],[]
-          | _ ->
-              error "Decreasing argument is not an inductive assumption.")
-      (* Unsupported cases *)
-      | Some (_,(CWfRec _|CMeasureRec _)) ->
-          error "Only structural decreasing is supported for mutual statements."
-      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
-      | None | Some (None, CStructRec) ->
       let whnf_hyp_hds = map_rel_context_in_env
         (fun env c -> fst (whd_all_stack env Evd.empty c))
         (Global.env()) hyps in
@@ -178,7 +162,7 @@ let find_mutually_recursive_statements thms =
     (finite,guard,None), ordered_inds
 
 let look_for_possibly_mutual_statements = function
-  | [id,(t,impls,None)] ->
+  | [id,(t,impls)] ->
       (* One non recursively proved theorem *)
       None,[id,(t,impls)],None
   | _::_ as thms ->
@@ -458,7 +442,7 @@ let start_proof_com ?inference_hook kind thms hook =
 		    | None -> Evd.from_env env0
 		    | Some l -> Evd.from_ctx (Evd.make_evar_universe_context env0 l))
   in
-  let thms = List.map (fun (sopt,(bl,t,guard)) ->
+  let thms = List.map (fun (sopt,(bl,t)) ->
     let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     let flags = all_and_fail_flags in
@@ -467,8 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'),
-       guard)))
+       (ids, imps @ lift_implicits (List.length ids) imps'))))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ca03ba3f3a..07066d983d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -489,7 +489,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
 	  start_proof_and_print (local,p,DefinitionBody k)
-	    [Some (lid,pl), (bl,t,None)] hook
+	    [Some (lid,pl), (bl,t)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
@@ -2077,7 +2077,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,None)] false
+  | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t)] false
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacUnfocused -> vernac_unfocused ()
-- 
cgit v1.2.3


From 8a35d93061c67dcdbb12337b78fcb35d72957f51 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:33 +0200
Subject: Minor cosmetic commit.

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

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 6eb7037f84..f31fce8859 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1155,7 +1155,7 @@ let interp_fixpoint l ntns =
 
 let interp_cofixpoint l ntns =
   let (env,_,pl,evd),fix,info = interp_recursive false l ntns in
-  check_recursive false  env evd fix;
+  check_recursive false env evd fix;
   (fix,pl,Evd.evar_universe_context evd,info)
     
 let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-- 
cgit v1.2.3


From 21d308fc083ee395e7b1ff78e75ec3a1305cb2f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:12:44 +0200
Subject: Fixing several wrong computations of implicit arguments by position
 in the presence of let-ins.

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

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index f31fce8859..c24dbdf7c0 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl p red_option c ctypopt =
   let ctx = Evd.make_evar_universe_context env pl in
   let evdref = ref (Evd.from_ctx ctx) in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
-  let nb_args = List.length ctx in
+  let nb_args = Context.Rel.nhyps ctx in
   let imps,pl,ce =
     match ctypopt with
       None ->
@@ -838,7 +838,7 @@ type structured_fixpoint_expr = {
 let interp_fix_context env evdref isfix fix =
   let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
   let impl_env, ((env', ctx), imps) = interp_context_evars env evdref before in
-  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(List.length before) env' evdref after in
+  let impl_env', ((env'', ctx'), imps') = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' evdref after in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
     ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
@@ -1100,7 +1100,7 @@ let interp_recursive isfix fixl notations =
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (nf_evar !evdref) fixtypes in
   let fiximps = List.map3
-    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (List.length ctx) cclimps))
+    (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
     fixctximps fixcclimps fixctxs in
   let rec_sign =
     List.fold_left2
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e7d1919ce0..430d48bc76 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -451,7 +451,7 @@ let start_proof_com ?inference_hook kind thms hook =
     let ids = List.map RelDecl.get_name ctx in
       (compute_proof_name (pi1 kind) sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
-       (ids, imps @ lift_implicits (List.length ids) imps'))))
+       (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
     thms in
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   let evd, nf = Evarutil.nf_evars_and_universes !evdref in
-- 
cgit v1.2.3


From 2ddc9d12bd4616f10245c40bc0c87ae548911809 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:58 +0200
Subject: Fixing #5420 as well as many related bugs due to miscounting let-ins.

- Supporting let-ins in tactic "fix", and hence in interactive
  Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
  presence of let-ins.
---
 vernac/command.ml  | 16 +++++++++-------
 vernac/command.mli |  8 ++++----
 vernac/lemmas.ml   |  4 ++--
 vernac/lemmas.mli  |  4 ++--
 4 files changed, 17 insertions(+), 15 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index c24dbdf7c0..a6343a5f5d 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -867,8 +867,10 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
 
 (* Jump over let-bindings. *)
 
-let compute_possible_guardness_evidences (ids,_,na) =
-  match na with
+let compute_possible_guardness_evidences (ctx,_,recindex) =
+  (* A recursive index is characterized by the number of lambdas to
+     skip before finding the relevant inductive argument *)
+  match recindex with
   | Some i -> [i]
   | None ->
       (* If recursive argument was not given by user, we try all args.
@@ -876,7 +878,7 @@ let compute_possible_guardness_evidences (ids,_,na) =
 	 but doing it properly involves delta-reduction, and it finally
          doesn't seem to worth the effort (except for huge mutual
 	 fixpoints ?) *)
-      List.interval 0 (List.length ids - 1)
+      List.interval 0 (Context.Rel.nhyps ctx - 1)
 
 type recursive_preentry =
   Id.t list * constr option list * types list
@@ -1136,10 +1138,10 @@ let interp_recursive isfix fixl notations =
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
-  let fixctxnames = List.map (fun (_,ctx) -> List.map RelDecl.get_name ctx) fixctxs in
+  let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in
 
   (* Build the fix declaration block *)
-  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots
+  (env,rec_sign,all_universes,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots
 
 let check_recursive isfix env evd (fixnames,fixdefs,_) =
   check_evars_are_solved env evd Evd.empty;
@@ -1162,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
@@ -1199,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
-      List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
+      List.map3 (fun id t (ctx,imps,_) -> ((id,pl),(t,(List.map RelDecl.get_name ctx,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
       Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC)
diff --git a/vernac/command.mli b/vernac/command.mli
index bccc22ae92..b62611e2e7 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -138,24 +138,24 @@ type recursive_preentry =
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
     recursive_preentry * lident list option * Evd.evar_universe_context * 
-    (Name.t list * Impargs.manual_implicits * int option) list
+    (Context.Rel.t * Impargs.manual_implicits * int option) list
 
 val interp_cofixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
     recursive_preentry * lident list option * Evd.evar_universe_context * 
-    (Name.t list * Impargs.manual_implicits * int option) list
+    (Context.Rel.t * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
-  (Name.t list * Impargs.manual_implicits * int option) list ->
+  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
-  (Name.t list * Impargs.manual_implicits * int option) list ->
+  (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 430d48bc76..ca511b573c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -100,10 +100,10 @@ let find_mutually_recursive_statements thms =
           match kind_of_term t with
           | Ind ((kn,_ as ind),u) when
                 let mind = Global.lookup_mind kn in
-                mind.mind_finite <> Decl_kinds.CoFinite && is_local_assum decl ->
+                mind.mind_finite <> Decl_kinds.CoFinite ->
               [ind,x,i]
           | _ ->
-              []) 0 (List.rev whnf_hyp_hds)) in
+              []) 0 (List.rev (List.filter RelDecl.is_local_assum whnf_hyp_hds))) in
       let ind_ccl =
         let cclenv = push_rel_context hyps (Global.env()) in
         let whnf_ccl,_ = whd_all_stack cclenv Evd.empty ccl in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 39c089be9f..6b45ed9339 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -41,8 +41,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 * universe_binders option) *
-     (types * (Name.t list * Impargs.manual_explicitation list))) list
+  ((Id.t (* name of thm *) * 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
 
 val universe_proof_terminator :
-- 
cgit v1.2.3


From 7d26940665ccce2e4ee1ba6fc157e42f7a639861 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 12 Apr 2017 12:15:40 +0200
Subject: Removing tactic compatibility layer in Command.

---
 vernac/command.ml | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'vernac')

diff --git a/vernac/command.ml b/vernac/command.ml
index 45ff579552..b27d8a0a35 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1198,11 +1198,8 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
+      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
-    let init_tac =
-      Option.map (List.map Proofview.V82.tactic) init_tac
-    in
     let evd = Evd.from_ctx ctx in
     Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
       evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
@@ -1235,11 +1232,8 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
       List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps))))
 		fixnames fixtypes fiximps in
     let init_tac =
-      Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC)
+      Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
         fixdefs) in
-    let init_tac =
-      Option.map (List.map Proofview.V82.tactic) init_tac
-    in
     let evd = Evd.from_ctx ctx in
       Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
       evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
-- 
cgit v1.2.3


From 4abb41d008fc754f21916dcac9cce49f2d04dd6d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 24 Apr 2017 19:25:48 +0200
Subject: [toplevel] Use exception information for error printing.

This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.

However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479

Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.

This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
---
 vernac/topfmt.ml  | 23 +++++++++++++++++++++++
 vernac/topfmt.mli | 11 +++++++----
 2 files changed, 30 insertions(+), 4 deletions(-)

(limited to 'vernac')

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index c25dd55fb7..a1835959c2 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -260,6 +260,29 @@ let init_color_output () =
  *)
 let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
 
+
+(* This is specific to the toplevel *)
+let pr_loc loc =
+  if Loc.is_ghost loc then str"<unknown>"
+  else
+    let fname = loc.Loc.fname in
+    if CString.equal fname "" then
+      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+	   str"-" ++ int loc.ep ++ str":")
+    else
+      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+	   str", line " ++ int loc.line_nb ++ str", characters " ++
+	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+	   str":")
+
+let print_err_exn ?extra any =
+  let (e, info) = CErrors.push any in
+  let loc = Loc.get_loc info in
+  let msg_loc = pr_loc (Option.default Loc.ghost loc) in
+  let pre_hdr = pr_opt_no_spc (fun x -> x) extra ++ msg_loc in
+  let msg = CErrors.iprint (e, info) ++ fnl () in
+  std_logger ~pre_hdr Feedback.Error msg
+
 (* Output to file, used only in extraction so a candidate for removal *)
 let ft_logger old_logger ft ?loc level mesg =
   let id x = x in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 909dd70775..6c8e0ae2fa 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -36,19 +36,22 @@ val get_depth_boxes : unit -> int option
 val set_margin : int option -> unit
 val get_margin : unit -> int option
 
-(** Headers for tagging *)
-val err_hdr : Pp.std_ppcmds
-val ann_hdr : Pp.std_ppcmds
-
 (** Console display of feedback, we may add some location information *)
 val std_logger   : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
 val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit
 
+(** Color output *)
 val init_color_output : unit -> unit
 val clear_styles : unit -> unit
 val parse_color_config : string -> unit
 val dump_tags : unit -> (string * Terminal.style) list
 
+(** Error printing *)
+(* To be deprecated when we can fully move to feedback-based error
+   printing. *)
+val pr_loc : Loc.t -> Pp.std_ppcmds
+val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit
+
 (** [with_output_to_file file f x] executes [f x] with logging
     redirected to a file [file] *)
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 vernac/class.ml      | 4 ++--
 vernac/command.ml    | 4 ++--
 vernac/ind_tables.ml | 6 +++---
 vernac/metasyntax.ml | 2 +-
 4 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'vernac')

diff --git a/vernac/class.ml b/vernac/class.ml
index 95114ec396..104f3c1db5 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -311,7 +311,7 @@ let add_coercion_hook poly local ref =
   | Global -> false
   | Discharge -> assert false
   in
-  let () = try_add_new_coercion ref stre poly in
+  let () = try_add_new_coercion ref ~local:stre poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
@@ -324,6 +324,6 @@ let add_subclass_hook poly local ref =
   | Discharge -> assert false
   in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl stre poly
+  try_add_new_coercion_subclass cl ~local:stre poly
 
 let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly)
diff --git a/vernac/command.ml b/vernac/command.ml
index b27d8a0a35..b2f5755ce6 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -258,7 +258,7 @@ match local with
   let () = Universes.register_universe_binders gr pl in
   let () = assumption_message ident in
   let () = Typeclasses.declare_instance None false gr in
-  let () = if is_coe then Class.try_add_new_coercion gr local p in
+  let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = 
     if p (* polymorphic *) then Univ.UContext.instance ctx 
     else Univ.Instance.empty
@@ -752,7 +752,7 @@ let do_mutual_inductive indl poly prv finite =
   (* Declare the possible notations of inductive types *)
   List.iter Metasyntax.add_notation_interpretation ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes;
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194c..c6588684a4 100644
--- a/vernac/ind_tables.ml
+++ b/vernac/ind_tables.ml
@@ -151,7 +151,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let const = define mode id c mib.mind_polymorphic 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
+     (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff
 
 let define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
@@ -172,7 +172,7 @@ let define_mutual_scheme_base kind suff f mode names mind =
   consts,
   Safe_typing.add_private 
     (Safe_typing.private_con_of_scheme
-      kind (Global.safe_env()) (Array.to_list schemes))
+      ~kind (Global.safe_env()) (Array.to_list schemes))
     eff 
 
 let define_mutual_scheme kind mode names mind =
@@ -185,7 +185,7 @@ let find_scheme_on_env_too kind ind =
   let s = String.Map.find kind (Indmap.find ind !scheme_map) in
   s, Safe_typing.add_private
       (Safe_typing.private_con_of_scheme
-            kind (Global.safe_env()) [ind, s])
+            ~kind (Global.safe_env()) [ind, s])
       Safe_typing.empty_private_constants
 
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f805eeaa90..f86a0ef928 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1196,7 +1196,7 @@ let inNotation : notation_obj -> obj =
 (**********************************************************************)
 
 let with_lib_stk_protection f x =
-  let fs = Lib.freeze `No in
+  let fs = Lib.freeze ~marshallable:`No in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
     let reraise = CErrors.push reraise in
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 vernac/auto_ind_decl.ml |  2 --
 vernac/metasyntax.ml    |  2 +-
 vernac/record.ml        |  2 +-
 vernac/topfmt.ml        | 12 ------------
 4 files changed, 2 insertions(+), 16 deletions(-)

(limited to 'vernac')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b9c4c6cc5d..015552d680 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -28,8 +28,6 @@ open Proofview.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let out_punivs = Univ.out_punivs
-
 (**********************************************************************)
 (* Generic synthesis of boolean equality *)
 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index f86a0ef928..bb5be4cb05 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -527,7 +527,7 @@ let warn_skip_spaces_curly =
       (fun () ->strbrk "Skipping spaces inside curly brackets")
 
 let rec drop_spacing = function
-  | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
+  | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
   | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt
   | fmt -> fmt
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 8b4b7606fc..53722b8f61 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -216,7 +216,7 @@ let warning_or_error coe indsp err =
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
   if coe then user_err ~hdr:"structure" st;
-  Flags.if_verbose Feedback.msg_info (hov 0 st)
+  warn_cannot_define_projection (hov 0 st)
 
 type field_status =
   | NoProjection of Name.t
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index a1835959c2..e44b585d7f 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -106,8 +106,6 @@ module Tag = struct
 
 end
 
-type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
-
 let msgnl_with ?pre_hdr fmt strm =
   pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
@@ -283,16 +281,6 @@ let print_err_exn ?extra any =
   let msg = CErrors.iprint (e, info) ++ fnl () in
   std_logger ~pre_hdr Feedback.Error msg
 
-(* Output to file, used only in extraction so a candidate for removal *)
-let ft_logger old_logger ft ?loc level mesg =
-  let id x = x in
-  match level with
-  | Debug   -> msgnl_with ft (make_body id  dbg_hdr mesg)
-  | Info    -> msgnl_with ft (make_body id info_hdr mesg)
-  | Notice  -> msgnl_with ft mesg
-  | Warning -> old_logger ?loc level mesg
-  | Error   -> old_logger ?loc level mesg
-
 let with_output_to_file fname func input =
   (* XXX FIXME: redirect std_ft  *)
   (* let old_logger = !logger in *)
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 vernac/auto_ind_decl.ml | 2 --
 vernac/classes.ml       | 2 --
 vernac/obligations.mli  | 1 -
 vernac/search.ml        | 2 --
 vernac/search.mli       | 1 -
 5 files changed, 8 deletions(-)

(limited to 'vernac')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 015552d680..25091f7833 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -9,7 +9,6 @@
 (* This file is about the automatic generation of schemes about
    decidable equality, created by Vincent Siles, Oct 2007 *)
 
-open Tacmach
 open CErrors
 open Util
 open Pp
@@ -716,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec =
         ))), eff
 
 let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
-  let open EConstr in
   let list_id = list_id lnamesparrec in
     let avoid = ref [] in
       let first_intros =
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 8337199655..d515b0c9b2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -66,8 +66,6 @@ let _ =
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
 
-open Vernacexpr
-
 (** TODO: add subinstances *)
 let existing_instance glob g info =
   let c = global g in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 11366fe91b..a276f9f9a3 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -12,7 +12,6 @@ open Evd
 open Names
 open Pp
 open Globnames
-open Vernacexpr
 open Decl_kinds
 
 (** Forward declaration. *)
diff --git a/vernac/search.ml b/vernac/search.ml
index 6279b17ae0..5b6e9a9c3c 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -14,11 +14,9 @@ open Declarations
 open Libobject
 open Environ
 open Pattern
-open Printer
 open Libnames
 open Globnames
 open Nametab
-open Goptions
 
 module NamedDecl = Context.Named.Declaration
 
diff --git a/vernac/search.mli b/vernac/search.mli
index 82b79f75de..e34522d8af 100644
--- a/vernac/search.mli
+++ b/vernac/search.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Environ
-- 
cgit v1.2.3


From 9a48211ea8439a8502145e508b70ede9b5929b2f Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 27 Apr 2017 21:58:52 +0200
Subject: Post-rebase warnings (unused opens and 2 unused values)

---
 vernac/topfmt.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index e44b585d7f..6d9d71a62b 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -131,7 +131,6 @@ let  dbg_hdr = tag Tag.debug   (str "Debug:")   ++ spc ()
 let info_hdr = mt ()
 let warn_hdr = tag Tag.warning (str "Warning:") ++ spc ()
 let  err_hdr = tag Tag.error   (str "Error:")   ++ spc ()
-let  ann_hdr = tag Tag.error   (str "Anomaly:") ++ spc ()
 
 let make_body quoter info ?pre_hdr s =
   pr_opt_no_spc (fun x -> x ++ fnl ()) pre_hdr ++ quoter (hov 0 (info ++ s))
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 vernac/auto_ind_decl.ml | 4 ++--
 vernac/obligations.ml   | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'vernac')

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b9c4c6cc5d..c91dcc5057 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -95,7 +95,7 @@ let destruct_on_using c id =
 let destruct_on_as c l =
   destruct false None c (Some (dl,l)) None
 
-(* reconstruct the inductive with the correct deBruijn indexes *)
+(* reconstruct the inductive with the correct de Bruijn indexes *)
 let mkFullInd (ind,u) n =
   let mib = Global.lookup_mind (fst ind) in
   let nparams = mib.mind_nparams in
@@ -174,7 +174,7 @@ let build_beq_scheme mode kn =
     (* give a type A, this function tries to find the equality on A declared
        previously *)
     (*  nlist = the number of args (A , B , ... )
-        eqA   = the deBruijn index of the first eq param
+        eqA   = the de Bruijn index of the first eq param
         ndx   = how much to translate due to the 2nd Case
     *)
     let compute_A_equality rel_list nlist eqA ndx t =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ea2401b5ce..e0520216b2 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -8,7 +8,7 @@ open Declare
 (**
    - Get types of existentials ;
    - Flatten dependency tree (prefix order) ;
-   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
    - Apply term prefixed by quantification on "existentials".
 *)
 
@@ -51,7 +51,7 @@ type oblinfo =
     ev_tac: unit Proofview.tactic option;
     ev_deps: Int.Set.t }
 
-(** Substitute evar references in t using De Bruijn indices,
+(** Substitute evar references in t using de Bruijn indices,
   where n binders were passed through. *)
 
 let subst_evar_constr evs n idf t =
@@ -102,7 +102,7 @@ let subst_evar_constr evs n idf t =
     t', !seen, !transparent
 
 
-(** Substitute variable references in t using De Bruijn indices,
+(** Substitute variable references in t using de Bruijn indices,
   where n binders were passed through. *)
 let subst_vars acc n t =
   let var_index id = Util.List.index Id.equal id acc in
-- 
cgit v1.2.3


From 6156fae91e69d379cfa0263a4c4cafb48da56f85 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 2 May 2017 16:09:56 +0200
Subject: Fix two new unused opens.

---
 vernac/lemmas.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1344701ff7..b79795aebd 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -28,10 +28,8 @@ open Pretyping
 open Termops
 open Namegen
 open Reductionops
-open Constrexpr
 open Constrintern
 open Impargs
-open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-- 
cgit v1.2.3


From 952e9aea47d3fad2d0f488d968ff0e90fa403ebc Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 3 May 2017 11:37:08 +0200
Subject: Adding an even more compact mode for goal display.

We want to print variables in vertical boxes as much as possible.

The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:

X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).
---
 vernac/vernacentries.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2cb6f3918f..40cd1a29c9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1411,6 +1411,24 @@ let _ =
       optread  = (fun _ -> None);
       optwrite = (fun _ -> ()) }
 
+let _ =
+  declare_int_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = Flags.print_hyps_limit;
+      optwrite = Flags.set_print_hyps_limit }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "display compact goal contexts";
+      optkey   = ["Printing";"Compact";"Contexts"];
+      optread  = (fun () -> Printer.get_compact_context());
+      optwrite = (fun b -> Printer.set_compact_context b) }
+
 let _ =
   declare_int_option
     { optsync  = true;
-- 
cgit v1.2.3


From 91d78c590b35c9edcf9f68c408ba82090f68e156 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 5 May 2017 12:59:41 +0200
Subject: Adapted to EConstr.

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

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 40cd1a29c9..d4e6af9959 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1411,15 +1411,6 @@ let _ =
       optread  = (fun _ -> None);
       optwrite = (fun _ -> ()) }
 
-let _ =
-  declare_int_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "the hypotheses limit";
-      optkey   = ["Hyps";"Limit"];
-      optread  = Flags.print_hyps_limit;
-      optwrite = Flags.set_print_hyps_limit }
-
 let _ =
   declare_bool_option
     { optsync  = true;
-- 
cgit v1.2.3


From fa530442ba05e9b60efff9c726616ae00d6d09e7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 4 May 2017 18:30:38 +0200
Subject: Obligations shrinking: shrink abstraction too

---
 vernac/obligations.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e0520216b2..62c5943897 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -631,6 +631,16 @@ let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 let add_hint local prg cst =
   Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
 
+let it_mkLambda_or_LetIn_or_clean t ctx =
+  let open Context.Rel.Declaration in
+  let fold t decl =
+    if is_local_assum decl then mkLambda_or_LetIn decl t
+    else
+      if noccurn 1 t then subst1 mkProp t
+      else mkLambda_or_LetIn decl t
+  in
+  Context.Rel.fold_inside fold ctx ~init:t
+
 let declare_obligation prg obl body ty uctx =
   let body = prg.prg_reduce body in
   let ty = Option.map prg.prg_reduce ty in
@@ -664,7 +674,7 @@ let declare_obligation prg obl body ty uctx =
 	    if poly then
 	      Some (DefinedObl constant)
 	    else
-	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
+	      Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
 
 let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 		   notations obls impls kind reduce hook =
-- 
cgit v1.2.3


From e3550a0acc39e235e01a727267b12a7c06f23b2c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 26 Aug 2016 14:46:33 +0200
Subject: Uniformity of style for selecting plural or not; spacing for comma.

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

(limited to 'vernac')

diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e0520216b2..5233fab151 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1088,7 +1088,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
       progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 vernac/lemmas.ml | 11 +----------
 1 file changed, 1 insertion(+), 10 deletions(-)

(limited to 'vernac')

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index b79795aebd..0088b70790 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -280,13 +280,6 @@ let save_anonymous ?export_seff proof save_ident =
   check_anonymity id save_ident;
   save ?export_seff save_ident const cstrs pl do_guard persistence hook
 
-let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,(cstrs,pl),do_guard,_,hook = proof in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs pl do_guard
-      (Global, const.const_entry_polymorphic, Proof kind) hook
-
 (* Admitted *)
 
 let warn_let_as_axiom =
@@ -337,9 +330,7 @@ let universe_proof_terminator compute_guard hook =
 	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
-      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
-      | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength ~export_seff proof kind id
+      | Some (_,id) -> save_anonymous ~export_seff proof id
       end;
       check_exist exports
   end
-- 
cgit v1.2.3