[classes] remove program mode from the new_instance_* APIs

4 files changed, 29 insertions, 37 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index caeedadbf4..792cd5f9ef 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1795,8 +1795,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
-  let program_mode = atts.program in
-  let _id = Classes.new_instance ~program_mode atts.polymorphic
+  let _id = Classes.new_instance atts.polymorphic
       name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
@@ -2025,7 +2024,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   let _id, pstate = Classes.new_instance_interactive
-      ~program_mode:atts.program ~global:atts.global atts.polymorphic
+      ~global:atts.global atts.polymorphic
       instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 2ef30e770c..763876b5c0 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -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 ~program_mode cty k u ctx ctx' pri decl imps subst id =
+let do_instance_interactive env 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,19 +476,19 @@ let do_instance_interactive env env' sigma ?hook ~tac ~global ~poly ~program_mod
         id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
     ()
 
-let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~tac ~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 }) ->
       if List.length fs > List.length k.cl_props then
         mismatched_props env' (List.map snd fs) k.cl_props;
-      let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in
+      let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in
       let term, termtype =
         do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
       term, termtype, sigma
     | (_, term) ->
       let sigma, def =
-        interp_casted_constr_evars ~program_mode env' sigma term cty in
+        interp_casted_constr_evars ~program_mode:false env' sigma term cty in
       let termtype = it_mkProd_or_LetIn cty ctx in
       let term = it_mkLambda_or_LetIn def ctx in
       term, termtype, sigma in
@@ -499,26 +499,26 @@ let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ct
     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 ~program_mode cty k u ctx ctx' pri decl imps subst id opt_props =
+let do_instance_program env env' sigma ?hook ~tac ~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 }) ->
       if List.length fs > List.length k.cl_props then
         mismatched_props env' (List.map snd fs) k.cl_props;
       let subst, sigma =
-        do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode subst in
+        do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in
      let term, termtype =
        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
      Some term, termtype, sigma
     | Some (_, term) ->
       let sigma, def =
-        interp_casted_constr_evars ~program_mode env' sigma term cty in
+        interp_casted_constr_evars ~program_mode:true env' sigma term cty in
       let termtype = it_mkProd_or_LetIn cty ctx in
       let term = it_mkLambda_or_LetIn def ctx in
       Some term, termtype, sigma
     | None ->
       let subst, sigma =
-        do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode subst in
+        do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in
       let term, termtype =
         do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
       Some term, termtype, sigma in
@@ -573,32 +573,32 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
   let env' = push_rel_context ctx env in
   id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
 
-let new_instance_interactive ?(global=false) ~program_mode
+let new_instance_interactive ?(global=false)
     poly instid ctx cl
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    new_instance_common ~program_mode ~generalize env instid ctx cl in
-  id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly ~program_mode
+    new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+  id, do_instance_interactive env env' sigma ?hook ~tac ~global ~poly
     cty k u ctx ctx' pri decl imps subst id
 
-let new_instance_program ?(global=false) ~program_mode
+let new_instance_program ?(global=false)
     poly instid ctx cl opt_props
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    new_instance_common ~program_mode ~generalize env instid ctx cl in
-  do_instance_program env env' sigma ?hook ~tac ~global ~poly ~program_mode
+    new_instance_common ~program_mode:true ~generalize env instid ctx cl in
+  do_instance_program env env' sigma ?hook ~tac ~global ~poly
     cty k u ctx ctx' pri decl imps subst id opt_props;
   id
 
-let new_instance ?(global=false) ~program_mode
+let new_instance ?(global=false)
     poly instid ctx cl props
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
-    new_instance_common ~program_mode ~generalize env instid ctx cl in
-  do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode
+    new_instance_common ~program_mode:false ~generalize env instid ctx cl in
+  do_instance env env' sigma ?hook ~tac ~global ~poly
     cty k u ctx ctx' pri decl imps subst id props;
   id
 
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 9572cd9598..3ec4325848 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -33,7 +33,6 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 
 val new_instance_interactive :
   ?global:bool (** Not global by default. *)
-  -> program_mode:bool
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
@@ -46,7 +45,6 @@ val new_instance_interactive :
 
 val new_instance :
   ?global:bool (** Not global by default. *)
-  -> program_mode:bool
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
@@ -60,7 +58,6 @@ val new_instance :
 
 val new_instance_program :
   ?global:bool (** Not global by default. *)
-  -> program_mode:bool
   -> Decl_kinds.polymorphic
   -> name_decl
   -> local_binder_expr list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9859bb62f0..2165f7c3ef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1085,40 +1085,36 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance_common ~atts name =
-  let open DefAttributes in
-  let global = not (make_section_locality atts.locality) in
-  Dumpglob.dump_constraint (fst name) false "inst";
-  let program_mode = atts.program in
-  program_mode, global
-
 let vernac_instance_interactive ~atts name bl t pri =
   let open DefAttributes in
-  let program_mode, global = vernac_instance_common ~atts name in
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let global = not (make_section_locality atts.locality) in
   let _id, pstate =
     Classes.new_instance_interactive
-      ~program_mode ~global atts.polymorphic name bl t pri in
+      ~global atts.polymorphic name bl t pri in
   pstate
 
 let vernac_instance_program ~atts name bl t opt_props pri =
   let open DefAttributes in
-  let program_mode, global = vernac_instance_common ~atts name in
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let global = not (make_section_locality atts.locality) in
   let _id = Classes.new_instance_program
-    ~program_mode ~global atts.polymorphic name bl t opt_props pri in
+    ~global atts.polymorphic name bl t opt_props pri in
   ()
 
 let vernac_instance ~atts name bl t props pri =
   let open DefAttributes in
-  let program_mode, global = vernac_instance_common ~atts name in
+  Dumpglob.dump_constraint (fst name) false "inst";
+  let global = not (make_section_locality atts.locality) in
   let _id =
     Classes.new_instance
-      ~program_mode ~global atts.polymorphic name bl t props pri in
+      ~global atts.polymorphic name bl t props pri in
   ()
 
 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 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 vernac_context ~poly l =