Merge PR #9270: Turn `Refine instance Mode` off by default

Ack-by: SkySkimmer
Ack-by: maximedenes
Reviewed-by: ppedrot

16 files changed, 132 insertions, 87 deletions

diff --git a/CHANGES.md b/CHANGES.md
index ae67eb5d1b..bcdb951a94 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -96,6 +96,11 @@ Vernacular commands
 - Computation of implicit arguments now properly handles local definitions in the
   binders for an `Instance`.
 
+- `Declare Instance` now requires an instance name.
+
+- Option `Refine Instance Mode` has been turned off by default, meaning that
+  `Instance` no longer opens a proof when a body is provided.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bb52f599a..2055b25ff4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
-           (Some (true, CAst.make @@ CRecord []))
+     None
     ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 169d608d2d..1641adbb70 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -3006,7 +3006,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
               let bname = VCS.mk_branch_name x in
               let opacity_of_produced_term = function
                 (* This AST is ambiguous, hence we check it dynamically *)
-                | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+                | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
                 | _ -> Doesn'tGuaranteeOpacity in
               VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
               let proof_mode = default_proof_mode () in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 454a4b66e7..09f531ce13 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -160,11 +160,12 @@ let classify_vernac e =
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _
     | VernacDeclareReduction _
-    | VernacDeclareClass _ | VernacDeclareInstances _
+    | VernacExistingClass _ | VernacExistingInstance _
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacDeclareCustomEntry _
-    | VernacComments _ -> VtSideff [], VtLater
+    | VernacComments _
+    | VernacDeclareInstance _ -> VtSideff [], VtLater
     (* Who knows *)
     | VernacLoad _ -> VtSideff [], VtNow
     (* (Local) Notations have to disappear *)
diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v
index 801c61b132..a321bb324e 100644
--- a/test-suite/bugs/closed/bug_2830.v
+++ b/test-suite/bugs/closed/bug_2830.v
@@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A).
 Admitted.
 
 Import FunctionalExtensionality.
-Instance set_cat : Category Type (fun A B => A -> B) := {
+
+Instance set_cat : Category Type (fun A B => A -> B).
+refine {|
   id := fun A => fun x => x
   ; comp c b a f g := fun x => f (g x)
   ; eqv := fun A B => @skel (A -> B)
-}.
+|}.
 intros. compute. symmetry. apply eta_expansion.
 intros. compute. symmetry. apply eta_expansion.
-intros. compute. reflexivity. Defined.
+intros. compute. reflexivity.
+Defined.
 
 (* The [list] type constructor is a Functor. *)
 
diff --git a/test-suite/bugs/closed/bug_3495.v b/test-suite/bugs/closed/bug_3495.v
index 7b0883f910..47db64a096 100644
--- a/test-suite/bugs/closed/bug_3495.v
+++ b/test-suite/bugs/closed/bug_3495.v
@@ -1,7 +1,7 @@
 Require Import RelationClasses.
 
 Axiom R : Prop -> Prop -> Prop.
-Declare Instance : Reflexive R.
+Declare Instance R_refl : Reflexive R.
 
 Class bar := { x : False }.
 Record foo := { a : Prop ; b : bar }.
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 379e46b3e3..9b3210860c 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -19,6 +19,6 @@ Class Category := {
 
 Require Export Coq.Setoids.Setoid.
 
-Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v
index 78b2aa69b9..9d83743b2a 100644
--- a/test-suite/bugs/opened/bug_3890.v
+++ b/test-suite/bugs/opened/bug_3890.v
@@ -3,7 +3,9 @@ Set Nested Proofs Allowed.
 Class Foo.
 Class Bar := b : Type.
 
+Set Refine Instance Mode.
 Instance foo : Foo := _.
+Unset Refine Instance Mode.
 (* 1 subgoals, subgoal 1 (ID 4)
 
   ============================
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 400479ae85..9086621344 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -198,7 +198,9 @@ Module UniqueInstances.
       for it. *)
   Set Typeclasses Unique Instances.
   Class Eq (A : Type) : Set.
+    Set Refine Instance Mode.
     Instance eqa : Eq nat := _. constructor. Qed.
+    Unset Refine Instance Mode.
     Instance eqb : Eq nat := {}.
     Class Foo (A : Type) (e : Eq A) : Set.
     Instance fooa : Foo _ eqa := {}.
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index 81a087b525..decb5c7519 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -12,3 +12,4 @@
 Local Set Warnings "-deprecated".
 
 Unset Private Polymorphic Universes.
+Set Refine Instance Mode.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index a342f5bf98..748a2628c5 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration
 open Decl_kinds
 open Entries
 
-let refine_instance = ref true
+let refine_instance = ref false
 
 let () = Goptions.(declare_bool_option {
   optdepr  = false;
@@ -105,8 +105,6 @@ let id_of_class cl =
 	  mip.(0).Declarations.mind_typename
     | _ -> assert false
 
-open Pp
-
 let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
   let info = intern_info info in
@@ -128,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
   instance_hook k info global imps ?hook (ConstRef kn)
 
-let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
   let subst = List.fold_left2
       (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
       [] subst (snd k.cl_context)
@@ -144,7 +142,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
          (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
   in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook k pri global imps ?hook (ConstRef cst); id
+  instance_hook k pri global imps (ConstRef cst)
 
 let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
   let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -191,7 +189,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
         else ignore (Pfedit.by (Tactics.auto_intros_tac ids));
         (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
 
-let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~refine ~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 }) ->
@@ -278,69 +276,74 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro
   else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
   id
 
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode
-    poly ctx (instid, bk, cl) props
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
-  let env = Global.env() in
-  let ({CAst.loc;v=instid}, pl) = instid in
+let interp_instance_context env ctx ?(generalize=false) pl bk cl =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass, ids =
     match bk with
     | Decl_kinds.Implicit ->
-	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
-	  (fun avoid (clname, _) ->
-	    match clname with
-            | Some cl ->
-                let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
-		  t, avoid
-	    | None -> failwith ("new instance: under-applied typeclass"))
-	  cl
+      Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
+        (fun avoid (clname, _) ->
+           match clname with
+           | Some cl ->
+             let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
+             t, avoid
+           | None -> failwith ("new instance: under-applied typeclass"))
+        cl
     | Explicit -> cl, Id.Set.empty
   in
   let tclass =
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
     else tclass
   in
-  let sigma, k, u, cty, ctx', ctx, imps, subst =
-    let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
-    let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
-    let len = Context.Rel.nhyps ctx in
-    let imps = imps @ Impargs.lift_implicits len imps' in
-    let ctx', c = decompose_prod_assum sigma c' in
-    let ctx'' = ctx' @ ctx in
-    let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
-    let u_s = EInstance.kind sigma u in
-    let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
-    let args = List.map of_constr args in
-    let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
-    let _, args =
-      List.fold_right (fun decl (args, args') ->
-	match decl with
-	| LocalAssum _ -> (List.tl args, List.hd args :: args')
+  let sigma, (impls, ((env', ctx), imps)) = interp_context_evars env sigma ctx in
+  let sigma, (c', imps') = interp_type_evars_impls ~impls env' sigma tclass in
+  let len = Context.Rel.nhyps ctx in
+  let imps = imps @ Impargs.lift_implicits len imps' in
+  let ctx', c = decompose_prod_assum sigma c' in
+  let ctx'' = ctx' @ ctx in
+  let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
+  let u_s = EInstance.kind sigma u in
+  let cl = Typeclasses.typeclass_univ_instance (k, u_s) in
+  let args = List.map of_constr args in
+  let cl_context = List.map (Termops.map_rel_decl of_constr) (snd cl.cl_context) in
+  let _, args =
+    List.fold_right (fun decl (args, args') ->
+        match decl with
+        | LocalAssum _ -> (List.tl args, List.hd args :: args')
         | LocalDef (_,b,_) -> (args, Vars.substl args' b :: args'))
-        cl_context (args, [])
-    in
-      sigma, cl, u, c', ctx', ctx, imps, args
+      cl_context (args, [])
+  in
+  let sigma = Evarutil.nf_evar_map sigma in
+  let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
+  sigma, cl, u, c', ctx', ctx, imps, args, decl
+
+
+let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
+    poly ctx (instid, bk, cl) props
+    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+  let env = Global.env() in
+  let ({CAst.loc;v=instid}, pl) = instid in
+  let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    interp_instance_context env ~generalize ctx pl bk cl
   in
   let id =
     match instid with
-	Name id ->
-	  let sp = Lib.make_path id in
-	    if Nametab.exists_cci sp then
-	      user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists.");
-	    id
-      | Anonymous ->
-	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
-	    Namegen.next_global_ident_away i (Termops.vars_of_env env)
+    | Name id -> id
+    | Anonymous ->
+      let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
+      Namegen.next_global_ident_away i (Termops.vars_of_env env)
   in
   let env' = push_rel_context ctx env in
-  let sigma = Evarutil.nf_evar_map sigma in
-  let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
-  if abstract then
-    do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
-  else
-    do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
-      cty k u ctx ctx' pri decl imps subst id props
+  do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+    cty k u ctx ctx' pri decl imps subst id props
+
+let declare_new_instance ?(global=false) poly ctx (instid, bk, cl) pri =
+  let env = Global.env() in
+  let ({CAst.loc;v=instid}, pl) = instid in
+  let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
+    interp_instance_context env ctx pl bk cl
+  in
+  do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
 
 let named_of_rel_context l =
   let open Vars in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index eb6c0c92e1..6f61da66cf 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -40,7 +40,6 @@ val declare_instance_constant :
   unit
 
 val new_instance :
-  ?abstract:bool (** Not abstract by default. *) ->
   ?global:bool (** Not global by default. *) ->
   ?refine:bool (** Allow refinement *) ->
   program_mode:bool ->
@@ -54,6 +53,14 @@ val new_instance :
   Hints.hint_info_expr ->
   Id.t
 
+val declare_new_instance :
+  ?global:bool (** Not global by default. *) ->
+  Decl_kinds.polymorphic ->
+  local_binder_expr list ->
+  ident_decl * Decl_kinds.binding_kind * constr_expr ->
+  Hints.hint_info_expr ->
+  unit
+
 (** Setting opacity *)
 
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 22528a607f..3bc4aecdb1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -683,19 +683,19 @@ GRAMMAR EXTEND Gram
 	 info = hint_info ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
 	     ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
-	   { VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) }
+	   { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) }
 
       | IDENT "Existing"; IDENT "Instance"; id = global;
           info = hint_info ->
-	  { VernacDeclareInstances [id, info] }
+	  { VernacExistingInstance [id, info] }
 
       | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
         pri = OPT [ "|"; i = natural -> { i } ] ->
          { let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
          let insts = List.map (fun i -> (i, info)) ids in
-	  VernacDeclareInstances insts }
+	  VernacExistingInstance insts }
 
-      | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is }
+      | IDENT "Existing"; IDENT "Class"; is = global -> { VernacExistingClass is }
 
       (* Arguments *)
       | IDENT "Arguments"; qid = smart_global; 
@@ -809,9 +809,8 @@ GRAMMAR EXTEND Gram
       | IDENT "transparent" -> { Conv_oracle.transparent } ] ]
   ;
   instance_name:
-    [ [ name = ident_decl; sup = OPT binders ->
-          { (CAst.map (fun id -> Name id) (fst name), snd name),
-          (Option.default [] sup) }
+    [ [ name = ident_decl; bl = binders ->
+          { (CAst.map (fun id -> Name id) (fst name), snd name), bl }
       | -> { ((CAst.make ~loc Anonymous), None), []  } ] ]
   ;
   hint_info:
@@ -845,10 +844,10 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "Comments"; l = LIST0 comment -> { VernacComments l }
 
       (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
-      | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
+      | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
 	 expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200";
 	 info = hint_info ->
-	   { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
+	   { VernacDeclareInstance (bl, (id, expl, t), info) }
 
       (* Should be in syntax, but camlp5 would not factorize *)
       | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e0dd3380f9..5eeeaada2d 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -887,10 +887,9 @@ open Pputils
               spc() ++ pr_class_rawexpr c2)
         )
 
-      | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
+      | VernacInstance (sup, (instid, bk, cl), props, info) ->
         return (
           hov 1 (
-            (if abst then keyword "Declare" ++ spc () else mt ()) ++
             keyword "Instance" ++
             (match instid with
              | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc ()
@@ -906,13 +905,23 @@ open Pputils
                 | None -> mt()))
         )
 
+      | VernacDeclareInstance (sup, (instid, bk, cl), info) ->
+        return (
+          hov 1 (
+            keyword "Declare Instance" ++ spc () ++ pr_ident_decl instid ++ spc () ++
+            pr_and_type_binders_arg sup ++
+              str":" ++ spc () ++
+              (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
+              pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info)
+        )
+
       | VernacContext l ->
         return (
           hov 1 (
             keyword "Context" ++ pr_and_type_binders_arg l)
         )
 
-      | VernacDeclareInstances insts ->
+      | VernacExistingInstance insts ->
          let pr_inst (id, info) =
            pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
          in
@@ -922,7 +931,7 @@ open Pputils
                  spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
         )
 
-      | VernacDeclareClass id ->
+      | VernacExistingClass id ->
         return (
           hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id)
         )
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dbccea1117..26859cd2cf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1005,22 +1005,29 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance ~atts abst sup inst props pri =
+let vernac_instance ~atts sup inst props pri =
   let open DefAttributes in
   let atts = parse atts in
   let global = not (make_section_locality atts.locality) in
   Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
   let program_mode = Flags.is_program_mode () in
-  ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
+  ignore(Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri)
+
+let vernac_declare_instance ~atts sup inst pri =
+  let open DefAttributes in
+  let atts = parse atts in
+  let global = not (make_section_locality atts.locality) in
+  Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
+  Classes.declare_new_instance ~global atts.polymorphic sup inst pri
 
 let vernac_context ~poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_declare_instances ~section_local insts =
+let vernac_existing_instance ~section_local insts =
   let glob = not section_local in
   List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
 
-let vernac_declare_class id =
+let vernac_existing_class id =
   Record.declare_existing_class (Nametab.global id)
 
 (***********)
@@ -2227,11 +2234,13 @@ let interp ?proof ~atts ~st c =
       vernac_identity_coercion ~atts id s t
 
   (* Type classes *)
-  | VernacInstance (abst, sup, inst, props, info) ->
-      vernac_instance ~atts abst sup inst props info
+  | VernacInstance (sup, inst, props, info) ->
+      vernac_instance ~atts sup inst props info
+  | VernacDeclareInstance (sup, inst, info) ->
+      vernac_declare_instance ~atts sup inst info
   | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
-  | VernacDeclareInstances insts -> with_section_locality ~atts vernac_declare_instances insts
-  | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id
+  | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
+  | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
 
   (* Solving *)
   | VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 417c9ebfbd..68a17e316e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -300,18 +300,22 @@ type nonrec vernac_expr =
 
   (* Type classes *)
   | VernacInstance of
-      bool * (* abstract instance *)
       local_binder_expr list * (* super *)
         typeclass_constraint * (* instance name, class name, params *)
         (bool * constr_expr) option * (* props *)
         Hints.hint_info_expr
 
+  | VernacDeclareInstance of
+      local_binder_expr list * (* super *)
+        (ident_decl * Decl_kinds.binding_kind * constr_expr) * (* instance name, class name, params *)
+        Hints.hint_info_expr
+
   | VernacContext of local_binder_expr list
 
-  | VernacDeclareInstances of
+  | VernacExistingInstance of
     (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
 
-  | VernacDeclareClass of qualid (* inductive or definition name *)
+  | VernacExistingClass of qualid (* inductive or definition name *)
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *