Merge PR #10185: Remove undocumented Instance : ! syntax

Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: vbgl

14 files changed, 83 insertions, 87 deletions

diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh
new file mode 100644
index 0000000000..c584438b21
--- /dev/null
+++ b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then
+
+    quickchick_CI_REF=instance-no-bang
+    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
+
+fi
diff --git a/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst
new file mode 100644
index 0000000000..c69cda9656
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/10185-instance-no-bang.rst
@@ -0,0 +1,2 @@
+- Remove undocumented :n:`Instance : !@type` syntax
+  (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert).
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 963b7189f9..5db8f999e5 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -30,7 +30,6 @@ open Evd
 open Tactypes
 open Locus
 open Locusops
-open Decl_kinds
 open Elimschemes
 open Environ
 open Termops
@@ -1791,15 +1790,15 @@ let rec strategy_of_ast = function
 let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l)
 
 let declare_an_instance n s args =
-  (((CAst.make @@ Name n),None), Explicit,
+  (((CAst.make @@ Name n),None),
    CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance ~pstate atts binders instance fields =
+let anew_instance ~pstate atts binders (name,t) fields =
   let program_mode = atts.program in
   new_instance ~pstate ~program_mode atts.polymorphic
-    binders instance (Some (true, CAst.make @@ CRecord (fields)))
+    name binders t (Some (true, CAst.make @@ CRecord (fields)))
     ~global:atts.global ~generalize:false Hints.empty_hint_info
 
 let declare_instance_refl ~pstate atts binders a aeq n lemma =
@@ -2014,16 +2013,18 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
 let add_morphism ~pstate atts binders m s n =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
-  let instance =
-    (((CAst.make @@ Name instance_id),None), Explicit,
-    CAst.make @@ CAppExpl (
-             (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
-             [cHole; s; m]))
+  let instance_name = (CAst.make @@ Name instance_id),None in
+  let instance_t =
+    CAst.make @@ CAppExpl
+      ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
+       [cHole; s; m])
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
-      None
-    ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in
+  let _, pstate = new_instance ~pstate
+      ~program_mode:atts.program ~global:atts.global atts.polymorphic
+      instance_name binders instance_t None
+      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
+  in
   pstate
 
 (** Bind to "rewrite" too *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 10f4865dfd..fc539b5208 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -580,7 +580,7 @@ end = struct (* {{{ *)
     (match Vernacprop.under_control x with
     | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
     | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
-    | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i
+    | VernacInstance (({CAst.v=Name i},_),_,_,_,_) -> Id.to_string i
     | _ -> "branch")
   let edit_branch = Branch.make "edit"
   let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 7cecd801e4..aa16f9535d 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -188,11 +188,11 @@ let classify_vernac e =
     | VernacDeclareMLModule _
     | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
     | VernacProofMode pm -> VtProofMode pm, VtNow
-    | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
+    | VernacInstance ((name,_),_,_,None,_) when not (Attributes.parse_drop_extra Attributes.program atts) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
       let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
       VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater
-    | VernacInstance (_,((name,_),_,_),_,_) ->
+    | VernacInstance ((name,_),_,_,_,_) ->
       VtSideff (idents_of_name name.CAst.v), VtLater
     (* Stm will install a new classifier to handle these *)
     | VernacBack _ | VernacAbortAll
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index c014ecc7ab..2dd254496b 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -337,7 +337,7 @@ Section Binary.
    morphism for equivalence (see Morphisms).  It is also sufficient to
    show that [R] is antisymmetric w.r.t. [eqA] *)
 
-  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R.
   Proof with auto.
     reduce_goal.
     apply H. firstorder.
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index e9a9d6aff2..7f26181108 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -94,7 +94,7 @@ Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
 Obligation Tactic := unfold complement, equiv ; program_simpl.
 
 Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
-  ! EqDec (prod A B) eq :=
+  EqDec (prod A B) eq :=
   { equiv_dec x y :=
     let '(x1, x2) := x in
     let '(y1, y2) := y in
@@ -115,7 +115,7 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
 (** Objects of function spaces with countable domains like bool have decidable
   equality. Proving the reflection requires functional extensionality though. *)
 
-Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
+Program Instance bool_function_eqdec `(EqDec A eq) : EqDec (bool -> A) eq :=
   { equiv_dec f g :=
     if f true == g true then
       if f false == g false then in_left
@@ -130,7 +130,7 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
 
 Require Import List.
 
-Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
+Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
   { equiv_dec :=
     fix aux (x y : list A) :=
     match x, y with
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 440b317573..3c0982cde7 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -464,7 +464,7 @@ Section Binary.
    morphism for equivalence (see Morphisms).  It is also sufficient to
    show that [R] is antisymmetric w.r.t. [eqA] *)
 
-  Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R.
+  Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric A eqA R.
   Proof with auto.
     reduce_goal.
     pose proof partial_order_equivalence as poe. do 3 red in poe.
@@ -481,7 +481,7 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type
 (** The partial order defined by subrelation and relation equivalence. *)
 
 Program Instance subrelation_partial_order :
-  ! PartialOrder (relation A) relation_equivalence subrelation.
+  PartialOrder (@relation_equivalence A) subrelation.
 
 Next Obligation.
 Proof.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 5a7f60584a..ea66234993 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -494,21 +494,8 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct
     else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
   id, pstate
 
-let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
+let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass =
   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
-    | Explicit -> cl, Id.Set.empty
-  in
   let tclass =
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
     else tclass
@@ -535,14 +522,13 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
   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 ~pstate ?(global=false) ~program_mode
-    poly ctx (instid, bk, cl) props
+    poly instid ctx 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 ~program_mode env ~generalize ctx pl bk cl
+    interp_instance_context ~program_mode env ~generalize ctx pl cl
   in
   let id =
     match instid with
@@ -555,10 +541,10 @@ let new_instance ~pstate ?(global=false) ~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 =
+let declare_new_instance ?(global=false) ~program_mode poly instid ctx 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 ~program_mode env ctx pl bk cl
+    interp_instance_context ~program_mode env ctx pl cl
   in
   do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 57bb9ce312..8d5f3e3a06 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -46,28 +46,29 @@ val declare_instance_constant :
   unit
 
 val new_instance :
-  pstate:Proof_global.t option ->
-  ?global:bool (** Not global by default. *) ->
-  program_mode:bool ->
-  Decl_kinds.polymorphic ->
-  local_binder_expr list ->
-  Vernacexpr.typeclass_constraint ->
-  (bool * constr_expr) option ->
-  ?generalize:bool ->
-  ?tac:unit Proofview.tactic  ->
-  ?hook:(GlobRef.t -> unit) ->
-  Hints.hint_info_expr ->
-  (* May open a proof *)
-  Id.t * Proof_global.t option
-
-val declare_new_instance :
-  ?global:bool (** Not global by default. *) ->
-  program_mode:bool ->
-  Decl_kinds.polymorphic ->
-  local_binder_expr list ->
-  ident_decl * Decl_kinds.binding_kind * constr_expr ->
-  Hints.hint_info_expr ->
-  unit
+  pstate:Proof_global.t option
+  -> ?global:bool (** Not global by default. *)
+  -> program_mode:bool
+  -> Decl_kinds.polymorphic
+  -> name_decl
+  -> local_binder_expr list
+  -> constr_expr
+  -> (bool * constr_expr) option
+  -> ?generalize:bool
+  -> ?tac:unit Proofview.tactic
+  -> ?hook:(GlobRef.t -> unit)
+  -> Hints.hint_info_expr
+  -> Id.t * Proof_global.t option (* May open a proof *)
+
+val declare_new_instance
+  : ?global:bool (** Not global by default. *)
+  -> program_mode:bool
+  -> Decl_kinds.polymorphic
+  -> ident_decl
+  -> local_binder_expr list
+  -> constr_expr
+  -> Hints.hint_info_expr
+  -> unit
 
 (** {6 Low level interface used by Add Morphism, do not use } *)
 val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 6438b48e32..b2db64f74c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -723,11 +723,11 @@ GRAMMAR EXTEND Gram
           { VernacContext (List.flatten c) }
 
       | IDENT "Instance"; namesup = instance_name; ":";
-	 expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200";
+         t = operconstr LEVEL "200";
 	 info = hint_info ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> { Some (true,r) } |
 	     ":="; c = lconstr -> { Some (false,c) } | -> { None } ] ->
-	   { VernacInstance (snd namesup,(fst namesup,expl,t),props,info) }
+           { VernacInstance (fst namesup,snd namesup,t,props,info) }
 
       | IDENT "Existing"; IDENT "Instance"; id = global;
           info = hint_info ->
@@ -888,9 +888,9 @@ GRAMMAR EXTEND Gram
 
       (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *)
       | IDENT "Declare"; IDENT "Instance"; id = ident_decl; bl = binders; ":";
-	 expl = [ "!" -> { Decl_kinds.Implicit } | -> { Decl_kinds.Explicit } ] ; t = operconstr LEVEL "200";
+         t = operconstr LEVEL "200";
 	 info = hint_info ->
-	   { VernacDeclareInstance (bl, (id, expl, t), info) }
+           { VernacDeclareInstance (id, bl, 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 f2332bab8b..2e97a169cc 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -911,7 +911,7 @@ open Pputils
               spc() ++ pr_class_rawexpr c2)
         )
 
-      | VernacInstance (sup, (instid, bk, cl), props, info) ->
+      | VernacInstance (instid, sup, cl, props, info) ->
         return (
           hov 1 (
             keyword "Instance" ++
@@ -920,7 +920,6 @@ open Pputils
              | { v = Anonymous }, _ -> mt ()) ++
             pr_and_type_binders_arg sup ++
               str":" ++ spc () ++
-              (match bk with Implicit -> str "! " | Explicit -> mt ()) ++
               pr_constr env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info ++
               (match props with
                 | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
@@ -929,13 +928,12 @@ open Pputils
                 | None -> mt()))
         )
 
-      | VernacDeclareInstance (sup, (instid, bk, cl), info) ->
+      | VernacDeclareInstance (instid, sup, 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 env sigma cl ++ pr_hint_info (pr_constr_pattern_expr env sigma) info)
         )
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 697bb788ac..828356d31d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1062,18 +1062,18 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance ~atts sup inst props pri =
+let vernac_instance ~atts name bl t props pri =
   let open DefAttributes in
   let global = not (make_section_locality atts.locality) in
-  Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
+  Dumpglob.dump_constraint (fst name) false "inst";
   let program_mode = atts.program in
-  Classes.new_instance ~program_mode ~global atts.polymorphic sup inst props pri
+  Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri
 
-let vernac_declare_instance ~atts sup inst pri =
+let vernac_declare_instance ~atts id bl inst pri =
   let open DefAttributes in
   let global = not (make_section_locality atts.locality) in
-  Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
-  Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
+  Dumpglob.dump_definition (fst id) false "inst";
+  Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri
 
 let vernac_context ~poly l =
   if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
@@ -2377,10 +2377,10 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
     pstate
 
   (* Type classes *)
-  | VernacInstance (sup, inst, props, info) ->
-    snd @@ with_def_attributes ~atts (vernac_instance ~pstate sup inst props info)
-  | VernacDeclareInstance (sup, inst, info) ->
-    with_def_attributes ~atts vernac_declare_instance sup inst info;
+  | VernacInstance (name, bl, t, props, info) ->
+    snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info)
+  | VernacDeclareInstance (id, bl, inst, info) ->
+    with_def_attributes ~atts vernac_declare_instance id bl inst info;
     pstate
   | VernacContext sup ->
     let () = vernac_context ~poly:(only_polymorphism atts) sup in
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 23633e39ab..f946e0596e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -303,15 +303,17 @@ type nonrec vernac_expr =
 
   (* Type classes *)
   | VernacInstance of
-      local_binder_expr list * (* super *)
-        typeclass_constraint * (* instance name, class name, params *)
-        (bool * constr_expr) option * (* props *)
-        Hints.hint_info_expr
+      name_decl * (* name *)
+      local_binder_expr list * (* binders *)
+      constr_expr * (* type *)
+      (bool * constr_expr) option * (* body (bool=true when using {}) *)
+      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
+      ident_decl * (* name *)
+      local_binder_expr list * (* binders *)
+      constr_expr * (* type *)
+      Hints.hint_info_expr
 
   | VernacContext of local_binder_expr list