Merge branch 'trunk' into located_switch

18 files changed, 113 insertions, 108 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index deb2ed3e0..bf274901b 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -44,6 +44,11 @@ let rec search_cst_label lab = function
   | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
   | _ :: fields -> search_cst_label lab fields
 
+let rec search_mind_label lab = function
+  | [] -> raise Not_found
+  | (l, SFBmind mind) :: _ when Label.equal l lab -> mind
+  | _ :: fields -> search_mind_label lab fields
+
 (* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But:
     a) I don't see currently what should be used instead
     b) this shouldn't be critical for Print Assumption. At worse some
@@ -135,6 +140,18 @@ let lookup_constant cst =
     else lookup_constant_in_impl cst (Some cb)
   with Not_found -> lookup_constant_in_impl cst None
 
+let lookup_mind_in_impl mind =
+  try
+    let mp,dp,lab = repr_kn (canonical_mind mind) in
+    let fields = memoize_fields_of_mp mp in
+      search_mind_label lab fields
+  with Not_found ->
+    anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind)
+
+let lookup_mind mind =
+  try Global.lookup_mind mind
+  with Not_found -> lookup_mind_in_impl mind
+
 (** Graph traversal of an object, collecting on the way the dependencies of
     traversed objects *)
 
@@ -227,7 +244,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
       where I_0, I_1, ... are in the same mutual definition and c_ij
       are all their constructors. *)
    if Refmap_env.mem firstind_ref data then data, ax2ty else
-     let mib = Global.lookup_mind mind in
+     let mib = lookup_mind mind in
      (* Collects references of parameters *)
      let param_ctx = mib.mind_params_ctxt in
      let nparam = List.length param_ctx in
@@ -331,7 +348,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
     else
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
-      let mind = Global.lookup_mind m in
+      let mind = lookup_mind m in
       if mind.mind_typing_flags.check_guarded then
         accu
       else
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index fd454b67e..31d610abd 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
@@ -28,8 +27,6 @@ open Proofview.Notations
 
 module RelDecl = Context.Rel.Declaration
 
-let out_punivs = Univ.out_punivs
-
 (**********************************************************************)
 (* Generic synthesis of boolean equality *)
 
@@ -93,7 +90,7 @@ let destruct_on_using c id =
 let destruct_on_as c l =
   destruct false None c (Some (Loc.tag 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
@@ -172,7 +169,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 =
@@ -716,7 +713,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/class.ml b/vernac/class.ml
index 95114ec39..104f3c1db 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/classes.ml b/vernac/classes.ml
index f9a3b01b6..884959c57 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/command.ml b/vernac/command.ml
index cae33f316..8a9bbb884 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -97,7 +97,7 @@ let interp_definition pl bl p red_option c ctypopt =
   let evdref = ref (Evd.from_ctx ctx) in
   let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
   let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
-  let nb_args = List.length ctx in
+  let nb_args = Context.Rel.nhyps ctx in
   let imps,pl,ce =
     match ctypopt with
       None ->
@@ -259,7 +259,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
@@ -753,7 +753,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 ()
 
@@ -850,7 +850,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)
 
@@ -881,8 +881,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.
@@ -890,7 +892,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
@@ -1131,7 +1133,7 @@ let interp_recursive isfix fixl notations =
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (fun c -> nf_evar !evdref c) 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
@@ -1170,10 +1172,10 @@ let interp_recursive isfix fixl notations =
   let fixdefs = List.map (fun c -> Option.map EConstr.Unsafe.to_constr c) fixdefs 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;
@@ -1189,21 +1191,18 @@ 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 =
   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 (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 _ _ -> ()))
@@ -1233,14 +1232,11 @@ 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 (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 _ _ -> ()))
diff --git a/vernac/command.mli b/vernac/command.mli
index 7cd0afeec..9bbc2fdac 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
+    (EConstr.rel_context * 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
+    (EConstr.rel_context * 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/ind_tables.ml b/vernac/ind_tables.ml
index 85d0b6194..c6588684a 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/lemmas.ml b/vernac/lemmas.ml
index c6f9f21d8..8dc444a43 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
@@ -88,25 +86,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 -> EConstr.Unsafe.to_constr (fst (whd_all_stack env Evd.empty (EConstr.of_constr c))))
         (Global.env()) hyps in
@@ -116,10 +98,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 (EConstr.of_constr ccl) in
@@ -178,7 +160,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 ->
@@ -298,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 =
@@ -355,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
@@ -458,7 +431,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 +440,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,
       (EConstr.Unsafe.to_constr (nf_evar !evdref (EConstr.it_mkProd_or_LetIn t' ctx)),
-       (ids, imps @ lift_implicits (List.length ids) imps'),
-       guard)))
+       (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
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 681413a29..d06b8fd14 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 :
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 83896992c..fb7c72941 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
 
@@ -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
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f0883e286..331b025f0 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
@@ -630,6 +630,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
@@ -663,7 +673,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 =
@@ -1087,7 +1097,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
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 11366fe91..a276f9f9a 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/record.ml b/vernac/record.ml
index 43a24e167..e33e1f8cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -217,7 +217,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/search.ml b/vernac/search.ml
index 6279b17ae..5b6e9a9c3 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 82b79f75d..e34522d8a 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
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 2f01cfb54..bbf2ed4fc 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -106,9 +106,7 @@ module Tag = struct
 
 end
 
-type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
-
-let msgnl_with fmt strm =
+let msgnl_with ?pre_hdr fmt strm =
   pp_with fmt (strm ++ fnl ());
   Format.pp_print_flush fmt ()
 
@@ -133,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))
@@ -260,15 +257,26 @@ let init_color_output () =
  *)
 let emacs_logger = gen_logger Emacs.quote_info Emacs.quote_warning
 
-(* 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
+
+(* This is specific to the toplevel *)
+let pr_loc loc =
+    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 = Option.cata pr_loc (mt ()) 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
 
 let with_output_to_file fname func input =
   (* XXX FIXME: redirect std_ft  *)
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index 909dd7077..6c8e0ae2f 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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a78350749..dc3bf6ba7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -477,7 +477,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
@@ -1412,6 +1412,15 @@ let _ =
       optwrite = (fun _ -> ()) }
 
 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;
       optdepr  = false;
@@ -2055,7 +2064,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 ()