Merge remote-tracking branch 'origin/master' into stm+doc_hook

33 files changed, 271 insertions, 262 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 9b8c4efb37..1ad5862d5d 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -82,9 +82,12 @@ let assert_empty k v =
   if v <> VernacFlagEmpty
   then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
 
+let error_twice ~name : 'a =
+  user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+
 let assert_once ~name prev =
   if Option.has_some prev then
-    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+    error_twice ~name
 
 let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
   let rec p extra v = function
@@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute =
   attribute_of_list [(on, single_key_parser ~name ~key:on true);
                (off, single_key_parser ~name ~key:off false)]
 
+(* Variant of the [bool] attribute with only two values (bool has three). *)
+let get_bool_value ~key ~default =
+  function
+  | VernacFlagEmpty -> default
+  | VernacFlagList [ "true", VernacFlagEmpty ] -> true
+  | VernacFlagList [ "false", VernacFlagEmpty ] -> false
+  | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.")
+
+let enable_attribute ~key ~default : bool attribute =
+  fun atts ->
+  let default = default () in
+  let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in
+  extra,
+  match this with
+  | [] -> default
+  | [ _, value ] -> get_bool_value ~key ~default:true value
+  | _ -> error_twice ~name:key
+
 let qualify_attribute qual (parser:'a attribute) : 'a attribute =
   fun atts ->
     let rec extract extra qualified = function
@@ -139,11 +160,8 @@ let () = let open Goptions in
       optread  = (fun () -> !program_mode);
       optwrite = (fun b -> program_mode:=b) }
 
-let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
-
-let program = program_opt >>= function
-  | Some b -> return b
-  | None -> return (!program_mode)
+let program =
+  enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
@@ -219,3 +237,6 @@ let only_polymorphism atts = parse polymorphic atts
 
 let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
 let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
+
+let canonical =
+  enable_attribute ~key:"canonical" ~default:(fun () -> true)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 3cb4d69ca0..44688ddafc 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -52,6 +52,7 @@ val program : bool attribute
 val template : bool option attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
+val canonical : bool attribute
 
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 9f233a2551..5a7f60584a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration
 open Decl_kinds
 open Entries
 
-let refine_instance = ref false
-
-let () = Goptions.(declare_bool_option {
-  optdepr  = true;
-  optname  = "definition of instances by refining";
-  optkey   = ["Refine";"Instance";"Mode"];
-  optread  = (fun () -> !refine_instance);
-  optwrite = (fun b -> refine_instance := b)
-})
-
 let set_typeclass_transparency c local b = 
   Hints.add_hints ~local [typeclasses_db]
     (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
@@ -328,6 +318,7 @@ let instance_hook k info global imps ?hook cst =
   (match hook with Some h -> h cst | None -> ())
 
 let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
+  (* XXX: Duplication of the declare_constant path *)
   let kind = IsDefinition Instance in
   let sigma =
     let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
@@ -349,14 +340,9 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma = Evd.minimize_universes sigma in
-  Pretyping.check_evars env (Evd.from_env env) sigma termtype;
-  let univs = Evd.check_univ_decl ~poly sigma decl in
-  let termtype = to_constr sigma termtype in
+  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
   let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
-      (ParameterEntry
-         (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-  in
+      (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook k pri global imps (ConstRef cst)
 
@@ -374,6 +360,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
     let obls, constr, typ =
       match term with
       | Some t ->
+        let termtype = EConstr.of_constr termtype in
         let obls, _, constr, typ =
           Obligations.eterm_obligations env id sigma 0 t termtype
         in obls, Some constr, typ
@@ -400,7 +387,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
           if not (Option.is_empty term) then
             let init_refine =
               Tacticals.New.tclTHENLIST [
-                Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term)));
+                Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term));
                 Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls);
                 Tactics.New.reduce_after_refine;
               ]
@@ -418,7 +405,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
         | None ->
           pstate) ())
 
-let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
   let props =
     match props with
     | Some (true, { CAst.v = CRecord fs }) ->
@@ -497,12 +484,12 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program
   (* Check that the type is free of evars now. *)
   Pretyping.check_evars env (Evd.from_env env) sigma termtype;
   let termtype = to_constr sigma termtype in
-  let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
   let pstate =
     if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
-      (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype;
+      let term = to_constr sigma (Option.get term) in
+      (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
        None)
-    else if program_mode || refine || Option.is_empty props then
+    else if program_mode || Option.is_empty props then
       declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
     else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
   id, pstate
@@ -549,7 +536,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
   sigma, cl, u, c', ctx', ctx, imps, args, decl
 
 
-let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode
+let new_instance ~pstate ?(global=false) ~program_mode
     poly ctx (instid, bk, cl) props
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
@@ -565,7 +552,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo
       Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
-  do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+  do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode
     cty k u ctx ctx' pri decl imps subst id props
 
 let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e7f90ff306..57bb9ce312 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -48,7 +48,6 @@ val declare_instance_constant :
 val new_instance :
   pstate:Proof_global.t option ->
   ?global:bool (** Not global by default. *) ->
-  ?refine:bool (** Allow refinement *) ->
   program_mode:bool ->
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 3406b6276f..635751bb24 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -43,7 +43,7 @@ let should_axiom_into_instance = function
     true
   | Global | Local -> !axiom_into_instance
 
-let declare_assumption ~pstate is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
+let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
 match local with
 | Discharge when Lib.sections_are_opened () ->
   let ctx = match ctx with
@@ -53,11 +53,6 @@ match local with
   let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
-  let () =
-    if not !Flags.quiet && Option.has_some pstate then
-    Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
-    strbrk " is not visible from current goals")
-  in
   let r = VarRef ident in
   let () = maybe_declare_manual_implicits true r imps in
   let env = Global.env () in
@@ -101,11 +96,11 @@ let next_uctx =
   | Polymorphic_entry _ as uctx -> uctx
   | Monomorphic_entry _ -> empty_uctx
 
-let declare_assumptions ~pstate idl is_coe k (c,uctx) pl imps nl =
+let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
   let refs, status, _ =
     List.fold_left (fun (refs,status,uctx) id ->
       let ref',u',status' =
-        declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in
+        declare_assumption is_coe k (c,uctx) pl imps false nl id in
       (ref',u')::refs, status' && status, next_uctx uctx)
       ([],true,uctx) idl
   in
@@ -137,7 +132,7 @@ let process_assumptions_udecls kind l =
   in
   udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
 
-let do_assumptions ~pstate ~program_mode kind nl l =
+let do_assumptions ~program_mode kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let udecl, l = process_assumptions_udecls kind l in
@@ -173,12 +168,17 @@ let do_assumptions ~pstate ~program_mode kind nl l =
       uvars, (coe,t,imps))
       Univ.LSet.empty l
   in
+  (* XXX: Using `DeclareDef.prepare_parameter` here directly is not
+     possible as we indeed declare several parameters; however,
+     restrict_universe_context should be called in a centralized place
+     IMO, thus I think we should adapt `prepare_parameter` to handle
+     this case too. *)
   let sigma = Evd.restrict_universe_context sigma uvars in
   let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in
   let ubinders = Evd.universe_binders sigma in
   pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
       let t = replace_vars subst t in
-      let refs, status' = declare_assumptions ~pstate  idl is_coe kind (t,uctx) ubinders imps nl in
+      let refs, status' = declare_assumptions  idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
           (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
@@ -226,7 +226,7 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let context ~pstate poly l =
+let context poly l =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -291,12 +291,12 @@ let context ~pstate poly l =
       let decl = (Discharge, poly, Definitional) in
       let nstatus = match b with
       | None ->
-        pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
+        pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
+        let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 7c64317b70..8f37bc0ba4 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -16,8 +16,7 @@ open Decl_kinds
 (** {6 Parameters/Assumptions} *)
 
 val do_assumptions
-  :  pstate:Proof_global.t option
-  -> program_mode:bool
+  : program_mode:bool
   -> locality * polymorphic * assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
@@ -26,8 +25,7 @@ val do_assumptions
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption
-  :  pstate:Proof_global.t option
-  -> coercion_flag
+  : coercion_flag
   -> assumption_kind
   -> Constr.types Entries.in_universes_entry
   -> UnivNames.universe_binders
@@ -42,8 +40,7 @@ val declare_assumption
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
 val context
-  :  pstate:Proof_global.t option
-  -> Decl_kinds.polymorphic
+  : Decl_kinds.polymorphic
   -> local_binder_expr list
   -> bool
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index feaf47df18..4cae4b8a74 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Entries
 open Redexpr
-open Declare
 open Constrintern
 open Pretyping
 
@@ -42,10 +41,9 @@ let check_imps ~impsty ~impsbody =
   if not b then warn_implicits_in_term ()
 
 let interp_definition ~program_mode pl bl poly red_option c ctypopt =
-  let open EConstr in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
-  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
   (* Build the parameters *)
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
   (* Build the type *)
@@ -66,31 +64,22 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
   in
   (* Do the reduction *)
   let evd, c = red_constant_body red_option env_bl evd c in
-  (* universe minimization *)
-  let evd = Evd.minimize_universes evd in
-  (* Substitute evars and universes, and add parameters.
-     Note: in program mode some evars may remain. *)
-  let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
-  let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
-  let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in
-  (* Keep only useful universes. *)
-  let uvars_fold uvars c =
-    Univ.LSet.union uvars (universes_of_constr evd (of_constr c))
-  in
-  let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in
-  let evd = Evd.restrict_universe_context evd uvars in
-  (* Check we conform to declared universes *)
-  let uctx = Evd.check_univ_decl ~poly evd decl in
-  (* We're done! *)
-  let ce = definition_entry ?types:tyopt ~univs:uctx c in
-  (ce, evd, decl, imps)
+
+  (* Declare the definition *)
+  let c = EConstr.it_mkLambda_or_LetIn c ctx in
+  let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
+
+  let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode
+      ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in
+
+  (ce, evd, udecl, imps)
 
 let check_definition ~program_mode (ce, evd, _, imps) =
   let env = Global.env () in
   check_evars_are_solved ~program_mode env evd;
   ce
 
-let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
+let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
     interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
   in
@@ -99,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
     let (c,ctx), sideff = Future.force ce.const_entry_body in
     assert(Safe_typing.empty_private_constants = sideff);
     assert(Univ.ContextSet.is_empty ctx);
+    Obligations.check_evars env evd;
+    let c = EConstr.of_constr c in
     let typ = match ce.const_entry_type with
-      | Some t -> t
-      | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c))
+      | Some t -> EConstr.of_constr t
+      | None -> Retyping.get_type_of env evd c
     in
-    Obligations.check_evars env evd;
     let obls, _, c, cty =
       Obligations.eterm_obligations env ident evd 0 c typ
     in
@@ -114,4 +104,4 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
     let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-    ignore(DeclareDef.declare_definition ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps)
+    ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 12853d83e0..fa4860b079 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,8 +17,7 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  :  ontop:Proof_global.t option
-  -> program_mode:bool
+  : program_mode:bool
   -> ?hook:Lemmas.declaration_hook
   -> Id.t
   -> definition_kind
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1912646ffd..00f19f545c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -284,7 +284,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
     let ctx = Evd.check_univ_decl ~poly evd pl in
     let pl = Evd.universe_binders evd in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
-    ignore (List.map4 (DeclareDef.declare_fix ~ontop (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;
@@ -319,7 +319,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
     let evd = Evd.restrict_universe_context evd vars in
     let ctx = Evd.check_univ_decl ~poly evd pl in
     let pl = Evd.universe_binders evd in
-    ignore (List.map4 (DeclareDef.declare_fix ~ontop (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/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 20a2db7ca2..69e2a209eb 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = Lemmas.mk_hook (hook sigma) in
-  (* XXX: Grounding non-ground terms here... bad bad *)
-  let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
-  let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
+    Obligations.eterm_obligations env recname sigma 0 def typ
   in
   let ctx = Evd.evar_universe_context sigma in
     ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
@@ -246,7 +243,7 @@ let out_def = function
   | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")
 
 let collect_evars_of_term evd c ty =
-  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
+  let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
@@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns =
   let evd = nf_evar_map_undefined evd in
   let collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
-    let def =
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign)
-    and typ =
-      (* Worrying... *)
-      EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign)
-    in
+    let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
+    let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
       Obligations.eterm_obligations env id evm
-        (List.length rec_sign) def typ
-    in (id, def, typ, imps, evars)
+        (List.length rec_sign) def typ in
+    (id, def, typ, imps, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 052832244b..bdda3314ca 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -14,12 +14,6 @@ open Entries
 open Globnames
 open Impargs
 
-let warn_definition_not_visible =
-  CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
-    Pp.(fun ident ->
-        strbrk "Section definition " ++
-        Names.Id.print ident ++ strbrk " is not visible from current goals")
-
 let warn_local_declaration =
   CWarnings.create ~name:"local-declaration" ~category:"scope"
     Pp.(fun (id,kind) ->
@@ -33,12 +27,11 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
       let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
-      let () = if Option.has_some ontop then warn_definition_not_visible ident in
       VarRef ident
   | Discharge | Local | Global ->
       let local = get_locality ident ~kind:"definition" local in
@@ -57,9 +50,9 @@ let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
   end;
   gr
 
-let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition ~ontop f kind ?hook_data ce pl imps
+  declare_definition f kind ?hook_data ce pl imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 8e4f4bf7fb..c4500d0a6b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,8 +14,7 @@ open Decl_kinds
 val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
 
 val declare_definition
-  :  ontop:Proof_global.t option
-  -> Id.t
+  : Id.t
   -> definition_kind
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
   -> Safe_typing.private_constants Entries.definition_entry
@@ -24,8 +23,7 @@ val declare_definition
   -> GlobRef.t
 
 val declare_fix
-  :  ontop:Proof_global.t option
-  -> ?opaque:bool
+  : ?opaque:bool
   -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
   -> definition_kind
   -> UnivNames.universe_binders
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3f491d1dd4..6438b48e32 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -43,6 +43,7 @@ let query_command = Entry.create "vernac:query_command"
 
 let subprf = Entry.create "vernac:subprf"
 
+let quoted_attributes = Entry.create "vernac:quoted_attributes"
 let class_rawexpr = Entry.create "vernac:class_rawexpr"
 let thm_token = Entry.create "vernac:thm_token"
 let def_body = Entry.create "vernac:def_body"
@@ -75,13 +76,13 @@ let parse_compat_version = let open Flags in function
 }
 
 GRAMMAR EXTEND Gram
-  GLOBAL: vernac_control gallina_ext noedit_mode subprf;
+  GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
   vernac_control: FIRST
-    [ [ IDENT "Time"; c = located_vernac -> { VernacTime (false,c) }
-      | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
-      | IDENT "Timeout"; n = natural; v = located_vernac -> { VernacTimeout(n,v) }
-      | IDENT "Fail"; v = located_vernac -> { VernacFail v }
-      | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+    [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
+      | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
+      | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) }
+      | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v }
+      | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ]
     ]
   ;
   decorated_vernac:
@@ -147,9 +148,6 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
 
-  located_vernac:
-    [ [ v = vernac_control -> { CAst.make ~loc v } ] ]
-  ;
 END
 
 {
@@ -450,8 +448,12 @@ GRAMMAR EXTEND Gram
 *)
   (* ... with coercions *)
   record_field:
-  [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> { n } ];
-      ntn = decl_notation -> { (bd,pri),ntn } ] ]
+  [ [ attr = LIST0 quoted_attributes ;
+      bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ];
+      rf_notation = decl_notation -> {
+      let rf_canonical = attr |> List.flatten |> parse canonical in
+      let rf_subclass, rf_decl = bd in
+      rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ]
   ;
   record_fields:
     [ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
@@ -1004,6 +1006,9 @@ GRAMMAR EXTEND Gram
       | IDENT "Grammar"; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
 	  { PrintGrammar ent }
+      | IDENT "Custom"; IDENT "Grammar"; ent = IDENT ->
+          (* Should also be in "syntax" section *)
+          { PrintCustomGrammar ent }
       | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir }
       | IDENT "Modules" ->
           { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 082b22b373..b2382ce6fc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -150,6 +150,7 @@ let explicit_flags =
     [print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ]
 
 let with_diffs pm pn =
+  if not (Proof_diffs.show_diffs ()) then pm, pn else
   try
     let tokenize_string = Proof_diffs.tokenize_string in
     Pp_diff.diff_pp ~tokenize_string pm pn
@@ -1347,9 +1348,6 @@ let explain_pattern_matching_error env sigma = function
   | CannotInferPredicate typs ->
       explain_cannot_infer_predicate env sigma typs
 
-let map_pguard_error = map_pguard_error
-let map_ptype_error = map_ptype_error
-
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
       let e = map_ptype_error EConstr.of_constr e in
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index d0f42ea16b..d1c1c092e3 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -43,9 +43,4 @@ val explain_module_error : Modops.module_typing_error -> Pp.t
 val explain_module_internalization_error :
   Modintern.module_internalization_error -> Pp.t
 
-val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
-[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."]
-val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
-[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."]
-
 val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 1c7cc5e636..317cf487cc 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function
 	  List.interval 0 (List.length ((lam_assum c))))
 	  lemma_guard (Array.to_list fixdefs) in
 *)
-              let fold env eff =
-                try
-                  let _ = Environ.lookup_constant eff.seff_constant env in
-                  env
-                with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
-              in
-              let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in
+              let env = Safe_typing.push_private_constants env eff in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in
@@ -395,10 +389,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s
 	  maybe_declare_manual_implicits false ref imps;
           call_hook ?hook ctx [] strength ref) thms_data in
       let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let pstate, _ = Proof_global.with_current_proof (fun _ p ->
+      let pstate = Proof_global.simple_with_current_proof (fun _ p ->
           match init_tac with
-          | None -> p,(true,[])
-          | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in
+          | None -> p
+          | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in
       pstate
 
 let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 843296d24e..50914959dc 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -50,10 +50,10 @@ let pr_entry e =
   str (Buffer.contents entry_buf)
 
 let pr_registered_grammar name =
-  let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in
+  let gram = Pcoq.find_grammars_by_name name in
   match gram with
-  | None -> user_err Pp.(str "Unknown or unprintable grammar entry.")
-  | Some entries ->
+  | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.")
+  | entries ->
     let pr_one (Pcoq.AnyEntry e) =
       str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++
       pr_entry e
@@ -85,6 +85,8 @@ let pr_grammar = function
       pr_entry Pvernac.Vernac_.gallina_ext
   | name -> pr_registered_grammar name
 
+let pr_custom_grammar name = pr_registered_grammar ("constr:"^name)
+
 (**********************************************************************)
 (* Parse a format (every terminal starting with a letter or a single
    quote (except a single quote alone) must be quoted) *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 38dbdf7e41..6435df23c7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
 (** Print the Camlp5 state of a grammar *)
 
 val pr_grammar : string -> Pp.t
+val pr_custom_grammar : string -> Pp.t
 
 val check_infix_modifiers : syntax_modifier list -> unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1b1c618dc7..46c4422d17 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -39,7 +39,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: Constr.named_context;
+    ev_hyps: EConstr.named_context;
     ev_status: bool * Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
@@ -50,11 +50,11 @@ type oblinfo =
 (** Substitute evar references in t using de Bruijn indices,
   where n binders were passed through. *)
 
-let subst_evar_constr evs n idf t =
+let subst_evar_constr evm evs n idf t =
   let seen = ref Int.Set.empty in
   let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc_f Evar.equal id evs in
-  let rec substrec (depth, fixrels) c = match Constr.kind c with
+  let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
     | Evar (k, args) ->
 	let { ev_name = (id, idstr) ;
 	      ev_hyps = hyps ; ev_chop = chop } =
@@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t =
 	  in aux hyps args []
 	in
 	  if List.exists
-            (fun x -> match Constr.kind x with
+            (fun x -> match EConstr.kind evm x with
             | Rel n -> Int.List.mem n fixrels
             | _ -> false) args
           then
 	    transparent := Id.Set.add idstr !transparent;
-	  mkApp (idf idstr, Array.of_list args)
+          EConstr.mkApp (idf idstr, Array.of_list args)
     | Fix _ ->
-	Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
-    | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c
+        EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
+    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
   in
   let t' = substrec (0, []) t in
-    t', !seen, !transparent
+    EConstr.to_constr evm t', !seen, !transparent
 
 
 (** Substitute variable references in t using de Bruijn indices,
@@ -112,18 +112,18 @@ let subst_vars acc n t =
     to a product : forall H1 : t1, ..., forall Hn : tn, concl.
     Changes evars and hypothesis references to variable references.
 *)
-let etype_of_evar evs hyps concl =
+let etype_of_evar evm evs hyps concl =
   let open Context.Named.Declaration in
   let rec aux acc n = function
       decl :: tl ->
-	let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
+        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
 	let t'' = subst_vars acc 0 t' in
 	let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
 	let trans' = Id.Set.union trans trans' in
 	  (match decl with
             | LocalDef (id,c,_) ->
-		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
+                let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
 		let c' = subst_vars acc 0 c' in
                   mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
 		Int.Set.union s'' s',
@@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl =
             | LocalAssum (id,_) ->
                 mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
     | [] ->
-	let t', s, trans = subst_evar_constr evs n mkVar concl in
+        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
 	  subst_vars acc 0 t', s, trans
   in aux [] 0 (List.rev hyps)
 
@@ -151,7 +151,7 @@ let evar_dependencies evm oev =
   let one_step deps =
     Evar.Set.fold (fun ev s ->
       let evi = Evd.find evm ev in
-      let deps' = evars_of_filtered_evar_info evi in
+      let deps' = evars_of_filtered_evar_info evm evi in
       if Evar.Set.mem oev deps' then
         invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
       else Evar.Set.union deps' s)
@@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty =
       (fun (id, (n, nstr), ev) l ->
 	 let hyps = Evd.evar_filtered_context ev in
          let hyps = trunc_named_context nc_len hyps in
-         let hyps = EConstr.Unsafe.to_named_context hyps in
-         let concl = EConstr.Unsafe.to_constr ev.evar_concl in
-         let evtyp, deps, transp = etype_of_evar l hyps concl in
+         let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in
 	 let evtyp, hyps, chop =
 	   match chop_product fs evtyp with
 	   | Some t -> t, trunc_named_context fs hyps, fs
@@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty =
       evn []
   in
   let t', _, transparent = (* Substitute evar refs in the term by variables *)
-    subst_evar_constr evts 0 mkVar t 
+    subst_evar_constr evm evts 0 EConstr.mkVar t
   in
-  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
+  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
   let evars = 
     List.map (fun (ev, info) ->
       let { ev_name = (_, name); ev_status = force_status, status;
@@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty =
       in name, typ, src, (force_status, status), deps, tac) evts
   in
   let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
-  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
+  let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in
     Array.of_list (List.rev evars), (evnames, evmap), t', ty
 
 let hide_obligation () =
@@ -456,7 +454,7 @@ let obligation_substitution expand prg =
   let ints = intset_to (pred (Array.length obls)) in
   obl_substitution expand obls ints
 
-let declare_definition ~ontop prg =
+let declare_definition prg =
   let varsubst = obligation_substitution true prg in
   let body, typ = subst_prog varsubst prg in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
@@ -475,7 +473,7 @@ let declare_definition ~ontop prg =
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
-  DeclareDef.declare_definition ~ontop prg.prg_name
+  DeclareDef.declare_definition prg.prg_name
     prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =
@@ -554,7 +552,7 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
-  let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
@@ -761,7 +759,7 @@ let update_obls prg obls rem =
     else (
       match prg'.prg_deps with
       | [] ->
-          let kn = declare_definition ~ontop:None prg' in
+          let kn = declare_definition prg' in
 	    progmap_remove prg';
 	    Defined kn
       | l ->
@@ -1112,7 +1110,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
-    let cst = declare_definition ~ontop:None prg in
+    let cst = declare_definition prg in
       Defined cst)
   else (
     let len = Array.length obls in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index d25daeed9c..9214ddd4b9 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
 val eterm_obligations : env -> Id.t -> evar_map -> int ->
-  ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
+  ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types ->
   (Id.t * types * Evar_kinds.t Loc.located *
      (bool * Evar_kinds.obligation_definition_status) * Int.Set.t *
       unit Proofview.tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
-  * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
+  * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
     constr * types
     (* Translations from existential identifiers to obligation identifiers 
        and for terms with existentials to closed terms, given a 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 4e4d431e89..f2332bab8b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -446,15 +446,15 @@ open Pputils
     | Some true -> str" :>"
     | Some false -> str" :>>"
 
-  let pr_record_field ((x, pri), ntn) =
+  let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let prx = match x with
-      | (oc,AssumExpr (id,t)) ->
+      | AssumExpr (id,t) ->
         hov 1 (pr_lname id ++
                  pr_oc oc ++ spc() ++
                  pr_lconstr_expr env sigma t)
-      | (oc,DefExpr(id,b,opt)) -> (match opt with
+      | DefExpr(id,b,opt) -> (match opt with
           | Some t ->
             hov 1 (pr_lname id ++
                      pr_oc oc ++ spc() ++
@@ -476,6 +476,8 @@ open Pputils
       keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s
     | PrintGrammar ent ->
       keyword "Print Grammar" ++ spc() ++ str ent
+    | PrintCustomGrammar ent ->
+      keyword "Print Custom Grammar" ++ spc() ++ str ent
     | PrintLoadPath dir ->
       keyword "Print LoadPath" ++ pr_opt DirPath.print dir
     | PrintModules ->
@@ -1262,15 +1264,15 @@ let pr_vernac_attributes =
 
   let rec pr_vernac_control v =
     let return = tag_vernac v in
-    match v with
+    match v.v with
     | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
-    | VernacTime (_,{v}) ->
+    | VernacTime (_,v) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
-    | VernacRedirect (s, {v}) ->
+    | VernacRedirect (s, v) ->
       return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
-    | VernacTimeout(n,{v}) ->
+    | VernacTimeout(n,v) ->
       return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
-    | VernacFail {v} ->
+    | VernacFail v->
       return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
 
     let pr_vernac v =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index d474ef8637..4d9157089c 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
 
     let () =
       let open Extend in
-      let act_vernac v loc = Some CAst.(make ~loc v) in
+      let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
         Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4bf7c9f7bd..41a2e7fd6f 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
     val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
-    val main_entry : vernac_control CAst.t option Entry.t
+    val main_entry : vernac_control option Entry.t
     val red_expr : raw_red_expr Entry.t
     val hint_info : Hints.hint_info_expr Entry.t
   end
@@ -40,7 +40,7 @@ module Unsafe : sig
 end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
+val main_entry : proof_mode option -> vernac_control option Entry.t
 
 (** Grammar entry for tactics: proof mode(s).
   By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/record.ml b/vernac/record.ml
index 74e5a03659..f737a8c524 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -276,8 +276,13 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields =
   let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in
   Termops.substl_rel_context (subst @ subst') fields
 
+type projection_flags = {
+  pf_subclass: bool;
+  pf_canonical: bool;
+}
+
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
@@ -299,7 +304,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
   in
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,i,kinds,sp_projs,subst) coe decl impls ->
+      (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
         let fi = RelDecl.get_name decl in
         let ti = RelDecl.get_type decl in
 	let (sp_projs,i,subst) =
@@ -359,17 +364,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 	    in
 	    let refi = ConstRef kn in
 	    Impargs.maybe_declare_manual_implicits false refi impls;
-	    if coe then begin
+            if flags.pf_subclass then begin
 	      let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
 	    end;
 	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
             with NotDefinable why ->
-	      warning_or_error coe indsp why;
+              warning_or_error flags.pf_subclass indsp why;
 	      (None::sp_projs,i,NoProjection fi::subst) in
-      (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst))
-      (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
+      (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+      (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
 open Typeclasses
@@ -525,7 +530,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
     | _ ->
-      let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in
+      let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+                         List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
       let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Method ~name:[|binder_name|] record_data
       in
@@ -634,7 +640,7 @@ let declare_existing_class g =
 open Vernacexpr
 
 let check_unique_names records =
-  let extract_name acc (((_, bnd), _), _) = match bnd with
+  let extract_name acc (rf_decl, _) = match rf_decl with
       Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc
     | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
     | _ -> acc in
@@ -649,15 +655,15 @@ let check_unique_names records =
 let check_priorities kind records =
   let isnot_class = match kind with Class false -> false | _ -> true in
   let has_priority (_, _, _, cfs, _, _) =
-    List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
+    List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
   in
   if isnot_class && List.exists has_priority records then
     user_err Pp.(str "Priorities only allowed for type class substructures")
 
 let extract_record_data records =
   let map (is_coe, id, _, cfs, idbuild, s) =
-    let fs = List.map (fun (((_, f), _), _) -> f) cfs in
-    id.CAst.v, s, List.map snd cfs, fs
+    let fs = List.map fst cfs in
+    id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs
   in
   let data = List.map map records in
   let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
@@ -691,16 +697,19 @@ let definition_structure udecl kind ~template cum poly finite records =
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
-    let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
-    let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
+    let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
+    let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
     declare_class def cum ubinders univs id.CAst.v idbuild
       implpars params arity template implfs fields coers priorities
   | _ ->
     let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
     let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
     let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
-      let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
-      let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
+      let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
+          { pf_subclass = not (Option.is_empty rf_subclass);
+            pf_canonical = rf_canonical })
+          cfs
+      in
       id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index 12a2a765b5..24bb27e107 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -14,15 +14,20 @@ open Constrexpr
 
 val primitive_flag : bool ref
 
+type projection_flags = {
+  pf_subclass: bool;
+  pf_canonical: bool;
+}
+
 val declare_projections :
   inductive ->
   Entries.universes_entry ->
   ?kind:Decl_kinds.definition_object_kind ->
   Id.t ->
-  bool list ->
+  projection_flags list ->
   Impargs.manual_implicits list ->
   Constr.rel_context ->
-    (Name.t * bool) list * Constant.t option list
+    Recordops.proj_kind list * Constant.t option list
 
 val declare_structure_entry : Recordops.struc_tuple -> unit
 
@@ -33,7 +38,7 @@ val definition_structure :
   (coercion_flag *
   Names.lident *
   local_binder_expr list *
-  (local_decl_expr with_instance with_priority with_notation) list *
+  (local_decl_expr * record_field_attr) list *
   Id.t * constr_expr option) list ->
   GlobRef.t list
 
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 60b0bdc7e7..bf2efb2542 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -196,6 +196,18 @@ let init_tag_map styles =
 let default_styles () =
   init_tag_map (default_tag_map ())
 
+let set_emacs_print_strings () =
+  let open Terminal in
+  let diff = "diff." in
+  List.iter (fun b ->
+      let (name, attrs) = b in
+      if CString.is_sub diff name 0 then
+        tag_map := CString.Map.add name
+          { attrs with prefix = Some (Printf.sprintf "<%s>" name);
+                       suffix = Some (Printf.sprintf "</%s>" name) }
+          !tag_map)
+    (CString.Map.bindings !tag_map)
+
 let parse_color_config str =
   let styles = Terminal.parse str in
   init_tag_map styles
@@ -264,13 +276,13 @@ let make_printing_functions () =
     let (tpfx, ttag) = split_tag tag in
     if tpfx <> end_pfx then
       let style = get_style ttag in
-      match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in
+      match style.Terminal.prefix with Some s -> Format.pp_print_as ft 0 s | None -> () in
 
   let print_suffix ft tag =
     let (tpfx, ttag) = split_tag tag in
     if tpfx <> start_pfx then
       let style = get_style ttag in
-      match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in
+      match style.Terminal.suffix with Some s -> Format.pp_print_as ft 0 s | None -> () in
 
   print_prefix, print_suffix
 
@@ -413,7 +425,7 @@ let with_output_to_file fname func input =
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
-let pr_cmd_header {CAst.loc;v=com} =
+let pr_cmd_header com =
   let shorten s =
     if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
   in
@@ -423,7 +435,7 @@ let pr_cmd_header {CAst.loc;v=com} =
         | x -> x
       ) s
   in
-  let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+  let (start,stop) = Option.cata Loc.unloc (0,0) com.CAst.loc in
   let safe_pr_vernac x =
     try Ppvernac.pr_vernac x
     with e -> str (Printexc.to_string e) in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index b0e3b3772c..3d522a9e0f 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -46,6 +46,7 @@ val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
 val default_styles : unit -> unit
 val parse_color_config : string -> unit
 val dump_tags : unit -> (string * Terminal.style) list
+val set_emacs_print_strings : unit -> unit
 
 (** Initialization of interpretation of tags *)
 val init_terminal_output : color:bool -> unit
@@ -72,4 +73,4 @@ val print_err_exn : exn -> unit
     redirected to a file [file] *)
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
 
-val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
+val pr_cmd_header : Vernacexpr.vernac_control -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e44d68b87d..918852239a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -605,7 +605,7 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
         | Some r ->
           let sigma, env = get_current_or_global_context ~pstate in
           Some (snd (Hook.get f_interp_redexp env sigma r)) in
-      ComDefinition.do_definition ~ontop:pstate ~program_mode name
+      ComDefinition.do_definition ~program_mode name
         (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
       pstate
   )
@@ -632,7 +632,7 @@ let vernac_exact_proof ~pstate c =
   if not status then Feedback.feedback Feedback.AddedAxiom;
   pstate
 
-let vernac_assumption ~atts ~pstate discharge kind l nl =
+let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
   let global = local == Global in
@@ -642,7 +642,7 @@ let vernac_assumption ~atts ~pstate discharge kind l nl =
       List.iter (fun (lid, _) ->
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
-  let status = ComAssumption.do_assumptions ~pstate ~program_mode:atts.program kind nl l in
+  let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let is_polymorphic_inductive_cumulativity =
@@ -684,7 +684,7 @@ let vernac_record ~template udecl cum k poly finite records =
     let () =
       if Dumpglob.dump () then
         let () = Dumpglob.dump_definition id false "rec" in
-        let iter (((_, x), _), _) = match x with
+        let iter (x, _) = match x with
         | Vernacexpr.AssumExpr ({loc;v=Name id}, _) ->
           Dumpglob.dump_definition (make ?loc id) false "proj"
         | _ -> ()
@@ -743,7 +743,8 @@ let vernac_inductive ~atts cum lo finite indl =
     let (id, bl, c, l) = Option.get is_defclass in
     let (coe, (lid, ce)) = l in
     let coe' = if coe then Some true else None in
-    let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
+    let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
@@ -1074,8 +1075,8 @@ let vernac_declare_instance ~atts sup inst pri =
   Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
   Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
 
-let vernac_context ~pstate ~poly l =
-  if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
+let vernac_context ~poly l =
+  if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_existing_instance ~section_local insts =
   let glob = not section_local in
@@ -1230,16 +1231,13 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
   let clear_implicits_flag = List.mem `ClearImplicits flags in
   let default_implicits_flag = List.mem `DefaultImplicits flags in
   let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
+  let nomatch_flag = List.mem `ReductionDontExposeCase flags in
 
   let err_incompat x y =
     user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
 
   if assert_flag && rename_flag then
     err_incompat "assert" "rename";
-  if Option.has_some nargs_for_red && never_unfold_flag then
-    err_incompat "simpl never" "/";
-  if never_unfold_flag && List.mem `ReductionDontExposeCase flags then
-    err_incompat "simpl never" "simpl nomatch";
   if clear_scopes_flag && extra_scopes_flag then
     err_incompat "clear scopes" "extra scopes";
   if clear_implicits_flag && default_implicits_flag then
@@ -1384,19 +1382,24 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
       (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args)
   in
 
-  let rec narrow = function
-    | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl
-    | [] -> [] | _ :: tl -> narrow tl
-  in
-  let red_flags = narrow flags in
-  let red_modifiers_specified =
-    not (List.is_empty rargs) || Option.has_some nargs_for_red
-    || not (List.is_empty red_flags)
+  let red_behavior =
+    let open Reductionops.ReductionBehaviour in
+    match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with
+    | true, false, [], None -> Some NeverUnfold
+    | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch"
+    | true, _, _::_, _ -> err_incompat "simpl never" "!"
+    | true, _, _, Some _ -> err_incompat "simpl never" "/"
+    | false, false, [], None  -> None
+    | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red;
+                                               recargs = rargs;
+                                             })
+    | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red;
+                                                     recargs = rargs;
+                                                   })
   in
 
-  if not (List.is_empty rargs) && never_unfold_flag then
-    err_incompat "simpl never" "!";
 
+  let red_modifiers_specified = Option.has_some red_behavior in
 
   (* Actions *)
 
@@ -1423,8 +1426,8 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
     match sr with
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
-         section_local c
-         (rargs, Option.default ~-1 nargs_for_red, red_flags)
+         ~local:section_local c (Option.get red_behavior)
+
     | _ -> user_err
              (strbrk "Modifiers of the behavior of the simpl tactic "++
               strbrk "are relevant for constants only.")
@@ -1732,29 +1735,29 @@ let vernac_set_option ~local export table v = match v with
 
 let vernac_add_option key lv =
   let f = function
-    | StringRefValue s -> (get_string_table key)#add s
-    | QualidRefValue locqid -> (get_ref_table key)#add locqid
+    | StringRefValue s -> (get_string_table key).add (Global.env()) s
+    | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid
   in
   try List.iter f lv with Not_found -> error_undeclared_key key
 
 let vernac_remove_option key lv =
   let f = function
-  | StringRefValue s -> (get_string_table key)#remove s
-  | QualidRefValue locqid -> (get_ref_table key)#remove locqid
+  | StringRefValue s -> (get_string_table key).remove (Global.env()) s
+  | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid
   in
   try List.iter f lv with Not_found -> error_undeclared_key key
 
 let vernac_mem_option key lv =
   let f = function
-  | StringRefValue s -> (get_string_table key)#mem s
-  | QualidRefValue locqid -> (get_ref_table key)#mem locqid
+  | StringRefValue s -> (get_string_table key).mem (Global.env()) s
+  | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid
   in
   try List.iter f lv with Not_found -> error_undeclared_key key
 
 let vernac_print_option key =
-  try (get_ref_table key)#print
+  try (get_ref_table key).print ()
   with Not_found ->
-  try (get_string_table key)#print
+  try (get_string_table key).print ()
   with Not_found ->
   try print_option_value key
   with Not_found -> error_undeclared_key key
@@ -1882,6 +1885,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts =
   | PrintSectionContext qid -> print_sec_context_typ env sigma qid
   | PrintInspect n -> inspect env sigma n
   | PrintGrammar ent -> Metasyntax.pr_grammar ent
+  | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent
   | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
   | PrintModules -> print_modules ()
   | PrintModule qid -> print_module qid
@@ -2296,7 +2300,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     unsupported_attributes atts;
     vernac_require_open_proof ~pstate (vernac_exact_proof c)
   | VernacAssumption ((discharge,kind),nl,l) ->
-    with_def_attributes ~atts vernac_assumption ~pstate discharge kind l nl;
+    with_def_attributes ~atts vernac_assumption discharge kind l nl;
     pstate
   | VernacInductive (cum, priv, finite, l) ->
     vernac_inductive ~atts cum priv finite l;
@@ -2379,7 +2383,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     with_def_attributes ~atts vernac_declare_instance sup inst info;
     pstate
   | VernacContext sup ->
-    let () = vernac_context ~pstate ~poly:(only_polymorphism atts) sup in
+    let () = vernac_context ~poly:(only_polymorphism atts) sup in
     pstate
   | VernacExistingInstance insts ->
     with_section_locality ~atts vernac_existing_instance insts;
@@ -2599,7 +2603,7 @@ and vernac_load ?proof ~verbosely ~st fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   pstate
 
-and interp_control ?proof ~st = function
+and interp_control ?proof ~st v = match v with
   | { v=VernacExpr (atts, cmd) } ->
     interp_expr ?proof ~atts ~st cmd
   | { v=VernacFail v } ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 71cc29b6e1..12451370c8 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -23,7 +23,7 @@ val vernac_require :
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-  st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t
+  st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d0dae1aa53..23633e39ab 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -29,6 +29,7 @@ type printable =
   | PrintSectionContext of qualid
   | PrintInspect of int
   | PrintGrammar of string
+  | PrintCustomGrammar of string
   | PrintLoadPath of DirPath.t option
   | PrintModules
   | PrintModule of qualid
@@ -143,13 +144,17 @@ type decl_notation = lstring * constr_expr * scope_name option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
 type 'a with_coercion = coercion_flag * 'a
-type 'a with_instance = instance_flag * 'a
-type 'a with_notation = 'a * decl_notation list
-type 'a with_priority = 'a * int option
+(* Attributes of a record field declaration *)
+type record_field_attr = {
+  rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *)
+  rf_priority: int option; (* priority of the instance, if relevant *)
+  rf_notation: decl_notation list;
+  rf_canonical: bool; (* use this projection in the search for canonical instances *)
+  }
 type constructor_expr = (lident * constr_expr) with_coercion
 type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
-  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
+  | RecordDecl of lident option * (local_decl_expr * record_field_attr) list
 type inductive_expr =
   ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
     constructor_list_or_record_decl_expr
@@ -398,11 +403,12 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_control =
+type vernac_control_r =
   | VernacExpr of Attributes.vernac_flags * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
-  | VernacTime of bool * vernac_control CAst.t
-  | VernacRedirect of string * vernac_control CAst.t
-  | VernacTimeout of int * vernac_control CAst.t
-  | VernacFail of vernac_control CAst.t
+  | VernacTime of bool * vernac_control
+  | VernacRedirect of string * vernac_control
+  | VernacTimeout of int * vernac_control
+  | VernacFail of vernac_control
+and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ef06e59316..730f5fd6da 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -36,7 +36,6 @@ type vernac_type =
   | VtProofMode of string
   (* To be removed *)
   | VtMeta
-  | VtUnknown
 and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 4d89eaffd9..54e08d0e95 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -52,7 +52,6 @@ type vernac_type =
   | VtProofMode of string
   (* To be removed *)
   | VtMeta
-  | VtUnknown
 and vernac_start = opacity_guarantee * Names.Id.t list
 and vernac_sideff_type = Names.Id.t list
 and opacity_guarantee =
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 704c5b2170..b3490c7dc6 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,19 +13,20 @@
 
 open Vernacexpr
 
-let rec under_control = function
+let rec under_control v = v |> CAst.with_val (function
   | VernacExpr (_, c) -> c
-  | VernacRedirect (_,{CAst.v=c})
-  | VernacTime (_,{CAst.v=c})
-  | VernacFail {CAst.v=c}
-  | VernacTimeout (_,{CAst.v=c}) -> under_control c
+  | VernacRedirect (_,c)
+  | VernacTime (_,c)
+  | VernacFail c
+  | VernacTimeout (_,c) -> under_control c
+  )
 
-let rec has_Fail = function
+let rec has_Fail v = v |> CAst.with_val (function
   | VernacExpr _ -> false
-  | VernacRedirect (_,{CAst.v=c})
-  | VernacTime (_,{CAst.v=c})
-  | VernacTimeout (_,{CAst.v=c}) -> has_Fail c
-  | VernacFail _ -> true
+  | VernacRedirect (_,c)
+  | VernacTime (_,c)
+  | VernacTimeout (_,c) -> has_Fail c
+  | VernacFail _ -> true)
 
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
 let is_navigation_vernac_expr = function
@@ -38,17 +39,17 @@ let is_navigation_vernac_expr = function
 let is_navigation_vernac c =
   is_navigation_vernac_expr (under_control c)
 
-let rec is_deep_navigation_vernac = function
-  | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
-  | VernacRedirect (_, {CAst.v=c})
-  | VernacTimeout (_,{CAst.v=c}) | VernacFail {CAst.v=c} -> is_navigation_vernac c
-  | VernacExpr _ -> false
+let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
+  | VernacTime (_,c) -> is_deep_navigation_vernac c
+  | VernacRedirect (_, c)
+  | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
+  | VernacExpr _ -> false)
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = function
+let is_reset = CAst.with_val (function
   | VernacExpr ( _, VernacResetInitial)
   | VernacExpr (_, VernacResetName _) -> true
-  | _ -> false
+  | _ -> false)
 
 let is_debug cmd = match under_control cmd with
   | VernacSetOption (_, ["Ltac";"Debug"], _) -> true