Simplify vernacentries calls to classes, remove unused args, reject deprecated attribute

This code was significantly more complex than necessary.

3 files changed, 66 insertions, 86 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 763876b5c0..9cc8467c57 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -333,7 +333,7 @@ let declare_instance_constant info global imps ?hook id decl poly sigma term ter
   Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma);
   instance_hook info global imps ?hook (ConstRef kn)
 
-let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id =
+let do_declare_instance 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)
@@ -462,7 +462,7 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
         (push_rel_context ctx' env') sigma kcl_props props subst in
     res, sigma
 
-let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id =
+let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id =
   let term, termtype =
     if List.is_empty k.cl_props then
      let term, termtype =
@@ -476,7 +476,7 @@ let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly cty k u ctx
         id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
     ()
 
-let do_instance env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props =
   let term, termtype, sigma =
     match props with
     | (true, { CAst.v = CRecord fs }) ->
@@ -499,7 +499,7 @@ let do_instance env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri dec
     let term = to_constr sigma term in
     declare_instance_constant pri global imps ?hook id decl poly sigma term termtype
 
-let do_instance_program env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
+let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props =
   let term, termtype, sigma =
     match opt_props with
     | Some (true, { CAst.v = CRecord fs }) ->
@@ -529,7 +529,7 @@ let do_instance_program env env' sigma ?hook ~tac ~global ~poly cty k u ctx ctx'
   else
     declare_instance_program  env sigma ~global ~poly id pri imps decl term termtype
 
-let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass =
+let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass =
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
@@ -579,26 +579,26 @@ let new_instance_interactive ?(global=false)
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     new_instance_common ~program_mode:false ~generalize env instid ctx cl in
-  id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
+  id, do_instance_interactive env sigma ?hook ~tac ~global ~poly
     cty k u ctx ctx' pri decl imps subst id
 
 let new_instance_program ?(global=false)
     poly instid ctx cl opt_props
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+    ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     new_instance_common ~program_mode:true ~generalize env instid ctx cl in
-  do_instance_program env env' sigma ?hook ~tac ~global ~poly
+  do_instance_program env env' sigma ?hook ~global ~poly
     cty k u ctx ctx' pri decl imps subst id opt_props;
   id
 
 let new_instance ?(global=false)
     poly instid ctx cl props
-    ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
+    ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
     new_instance_common ~program_mode:false ~generalize env instid ctx cl in
-  do_instance env env' sigma ?hook ~tac ~global ~poly
+  do_instance env env' sigma ?hook ~global ~poly
     cty k u ctx ctx' pri decl imps subst id props;
   id
 
@@ -606,6 +606,6 @@ 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 cl
+    interp_instance_context ~program_mode ~generalize:false env ctx pl cl
   in
-  do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
+  do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 3ec4325848..e61935c87a 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -51,7 +51,6 @@ val new_instance :
   -> constr_expr
   -> (bool * constr_expr)
   -> ?generalize:bool
-  -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
   -> Id.t
@@ -64,7 +63,6 @@ val new_instance_program :
   -> constr_expr
   -> (bool * constr_expr) option
   -> ?generalize:bool
-  -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
   -> Hints.hint_info_expr
   -> Id.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2165f7c3ef..ca4b50318b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -64,6 +64,16 @@ let modify_pstate ~pstate f =
   vernac_require_open_proof ~pstate (fun ~pstate ->
       Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
 
+let with_read_proof ~pstate f =
+  f ~pstate;
+  pstate
+
+let with_open_proof ~pstate f =
+  Some (Proof_global.push ~ontop:pstate (f ~pstate))
+
+let with_open_proof_simple ~pstate f =
+  Some (Proof_global.push ~ontop:pstate f)
+
 let get_current_or_global_context ~pstate =
   match pstate with
   | None -> let env = Global.env () in Evd.(from_env env, env)
@@ -99,6 +109,25 @@ module DefAttributes = struct
     { polymorphic; program; locality; deprecated }
 end
 
+let with_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  f ~local
+
+let with_section_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  let section_local = make_section_locality local in
+  f ~section_local
+
+let with_module_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  let module_local = make_module_locality local in
+  f ~module_local
+
+let with_def_attributes ~atts f =
+  let atts = DefAttributes.parse atts in
+  if atts.DefAttributes.program then Obligations.check_program_libraries ();
+  f ~atts
+
 (*******************)
 (* "Show" commands *)
 
@@ -1085,37 +1114,33 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance_interactive ~atts name bl t pri =
-  let open DefAttributes in
+let vernac_instance ~pstate ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let global = not (make_section_locality atts.locality) in
-  let _id, pstate =
-    Classes.new_instance_interactive
-      ~global atts.polymorphic name bl t pri in
-  pstate
-
-let vernac_instance_program ~atts name bl t opt_props pri =
-  let open DefAttributes in
-  Dumpglob.dump_constraint (fst name) false "inst";
-  let global = not (make_section_locality atts.locality) in
-  let _id = Classes.new_instance_program
-    ~global atts.polymorphic name bl t opt_props pri in
-  ()
-
-let vernac_instance ~atts name bl t props pri =
-  let open DefAttributes in
-  Dumpglob.dump_constraint (fst name) false "inst";
-  let global = not (make_section_locality atts.locality) in
-  let _id =
-    Classes.new_instance
-      ~global atts.polymorphic name bl t props pri in
-  ()
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  if program then begin
+    let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in
+    pstate
+  end else begin
+    match props with
+    | None ->
+      with_open_proof_simple ~pstate
+        (let _id, pstate = Classes.new_instance_interactive ~global polymorphic name bl t info in
+         pstate)
+    | Some props ->
+      let _id : Id.t = Classes.new_instance ~global polymorphic name bl t props info in
+      pstate
+  end
 
 let vernac_declare_instance ~atts id bl inst pri =
-  let open DefAttributes in
   Dumpglob.dump_definition (fst id) false "inst";
-  let global = not (make_section_locality atts.locality) in
-  Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri
+  let (program, locality), polymorphic =
+    Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
+  in
+  let global = not (make_section_locality locality) in
+  Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri
 
 let vernac_context ~poly l =
   if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
@@ -2253,36 +2278,6 @@ let vernac_check_guard ~pstate =
       (str ("Condition violated: ") ++s)
   in message
 
-(* Attributes *)
-let with_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  f ~local
-
-let with_section_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  let section_local = make_section_locality local in
-  f ~section_local
-
-let with_module_locality ~atts f =
-  let local = Attributes.(parse locality atts) in
-  let module_local = make_module_locality local in
-  f ~module_local
-
-let with_def_attributes ~atts f =
-  let atts = DefAttributes.parse atts in
-  if atts.DefAttributes.program then Obligations.check_program_libraries ();
-  f ~atts
-
-let with_read_proof ~pstate f =
-  f ~pstate;
-  pstate
-
-let with_open_proof ~pstate f =
-  Some (Proof_global.push ~ontop:pstate (f ~pstate))
-
-let with_open_proof_simple ~pstate f =
-  Some (Proof_global.push ~ontop:pstate f)
-
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
@@ -2517,22 +2512,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
 
   (* Type classes *)
   | VernacInstance (name, bl, t, props, info) ->
-    if (DefAttributes.parse atts).DefAttributes.program then begin
-      with_def_attributes ~atts
-        (vernac_instance_program name bl t props info);
-      pstate
-    end else begin
-      match props with
-      | None ->
-        with_open_proof_simple ~pstate
-          (with_def_attributes ~atts
-            (vernac_instance_interactive name bl t info))
-      | Some props ->
-         with_def_attributes ~atts (vernac_instance name bl t props info);
-         pstate
-      end
+    vernac_instance ~pstate ~atts name bl t props info
   | VernacDeclareInstance (id, bl, inst, info) ->
-    with_def_attributes ~atts vernac_declare_instance id bl inst info;
+    vernac_declare_instance ~atts id bl inst info;
     pstate
   | VernacContext sup ->
     let () = vernac_context ~poly:(only_polymorphism atts) sup in