diff --git a/CHANGES.md b/CHANGES.md
index 1a0b53f84a2e..26573b918551 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -126,6 +126,10 @@ Vernacular commands
    class will have to be changed into `Instance foo : C := {}.` or
    `Instance foo : C. Proof. Qed.`.
 
+- Option `Program Mode` now means that the `Program` attribute is enabled
+  for all commands that support it. In particular, it does not have any effect
+  on tactics anymore. May cause some incompatibilities.
+
 Tools
 
 - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index db56d0628f5d..d70c009c6dac 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -337,6 +337,7 @@ type naming_mode =
   | KeepUserNameAndRenameExistingEvenSectionNames
   | KeepExistingNames
   | FailIfConflict
+  | ProgramNaming
 
 let push_rel_decl_to_named_context
   ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
@@ -364,7 +365,7 @@ let push_rel_decl_to_named_context
         using this function. For now, we only attempt to preserve the
         old behaviour of Program, but ultimately, one should do something
         about this whole name generation problem. *)
-    if Flags.is_program_mode () then next_name_away na avoid
+    if hypnaming = ProgramNaming then next_name_away na avoid
     else
       (* id_of_name_using_hdchar only depends on the rel context which is empty
          here *)
@@ -372,7 +373,8 @@ let push_rel_decl_to_named_context
   in
   match extract_if_neq id na with
   | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames ||
-                  hypnaming = KeepUserNameAndRenameExistingButSectionNames &&
+                  (hypnaming = KeepUserNameAndRenameExistingButSectionNames ||
+                   hypnaming = ProgramNaming) &&
                   not (is_section_variable id0) ->
       (* spiwack: if [id<>id0], rather than introducing a new
           binding named [id], we will keep [id0] (the name given
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 0e6747577862..23b240f1a0c6 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -38,6 +38,7 @@ type naming_mode =
   | KeepUserNameAndRenameExistingEvenSectionNames
   | KeepExistingNames
   | FailIfConflict
+  | ProgramNaming
 
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c8c38ffe0598..24894fc9f592 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2328,36 +2328,38 @@ let interp_open_constr env sigma c =
 
 (* Not all evars expected to be resolved and computation of implicit args *)
 
-let interp_constr_evars_gen_impls env sigma
+let interp_constr_evars_gen_impls ?(program_mode=false) env sigma
     ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env sigma c in
   let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:(expected_type == IsType) c in
-  let sigma, c = understand_tcc env sigma ~expected_type c in
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
   sigma, (c, imps)
 
-let interp_constr_evars_impls env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env sigma ~impls WithoutTypeConstraint c
+let interp_constr_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls ?program_mode env sigma ~impls WithoutTypeConstraint c
 
-let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c
+let interp_casted_constr_evars_impls ?program_mode env evdref ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen_impls ?program_mode env evdref ~impls (OfType typ) c
 
-let interp_type_evars_impls env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen_impls env sigma ~impls IsType c
+let interp_type_evars_impls ?program_mode env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen_impls ?program_mode env sigma ~impls IsType c
 
 (* Not all evars expected to be resolved, with side-effect on evars *)
 
-let interp_constr_evars_gen env sigma ?(impls=empty_internalization_env) expected_type c =
+let interp_constr_evars_gen ?(program_mode=false) env sigma ?(impls=empty_internalization_env) expected_type c =
   let c = intern_gen expected_type ~impls env sigma c in
-  understand_tcc env sigma ~expected_type c
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
+  understand_tcc ~flags env sigma ~expected_type c
 
-let interp_constr_evars env evdref ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c
+let interp_constr_evars ?program_mode env evdref ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen ?program_mode env evdref WithoutTypeConstraint ~impls c
 
-let interp_casted_constr_evars env sigma ?(impls=empty_internalization_env) c typ =
-  interp_constr_evars_gen env sigma ~impls (OfType typ) c
+let interp_casted_constr_evars ?program_mode env sigma ?(impls=empty_internalization_env) c typ =
+  interp_constr_evars_gen ?program_mode env sigma ~impls (OfType typ) c
 
-let interp_type_evars env sigma ?(impls=empty_internalization_env) c =
-  interp_constr_evars_gen env sigma IsType ~impls c
+let interp_type_evars ?program_mode env sigma ?(impls=empty_internalization_env) c =
+  interp_constr_evars_gen ?program_mode env sigma IsType ~impls c
 
 (* Miscellaneous *)
 
@@ -2419,8 +2421,9 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
-let interp_glob_context_evars env sigma k bl =
+let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
   let open EConstr in
+  let flags = { Pretyping.all_no_fail_flags with program_mode } in
   let env, sigma, par, _, impls =
     List.fold_left
       (fun (env,sigma,params,n,impls) (na, k, b, t) ->
@@ -2428,7 +2431,7 @@ let interp_glob_context_evars env sigma k bl =
 	 if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
 	 else t
        in
-       let sigma, t = understand_tcc env sigma ~expected_type:IsType t' in
+       let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in
 	match b with
 	    None ->
 	      let d = LocalAssum (na,t) in
@@ -2440,13 +2443,13 @@ let interp_glob_context_evars env sigma k bl =
 	      in
                 (push_rel d env, sigma, d::params, succ n, impls)
 	  | Some b ->
-              let sigma, c = understand_tcc env sigma ~expected_type:(OfType t) b in
+              let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in
 	      let d = LocalDef (na, c, t) in
                 (push_rel d env, sigma, d::params, n, impls))
       (env,sigma,[],k+1,[]) (List.rev bl)
   in sigma, ((env, par), impls)
 
-let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
+let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let sigma, x = interp_glob_context_evars env sigma shift bl in
+  let sigma, x = interp_glob_context_evars ?program_mode env sigma shift bl in
   sigma, (int_env, x)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 61acd09d65d2..2d14a0d0a7a6 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -113,26 +113,26 @@ val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr
 
 (** Accepting unresolved evars *)
 
-val interp_constr_evars : env -> evar_map ->
+val interp_constr_evars : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> evar_map * constr
 
-val interp_casted_constr_evars : env -> evar_map ->
+val interp_casted_constr_evars : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> types -> evar_map * constr
 
-val interp_type_evars : env -> evar_map ->
+val interp_type_evars : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> evar_map * types
 
 (** Accepting unresolved evars and giving back the manual implicit arguments *)
 
-val interp_constr_evars_impls : env -> evar_map ->
+val interp_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
   evar_map * (constr * Impargs.manual_implicits)
 
-val interp_casted_constr_evars_impls : env -> evar_map ->
+val interp_casted_constr_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr -> types ->
   evar_map * (constr * Impargs.manual_implicits)
 
-val interp_type_evars_impls : env -> evar_map ->
+val interp_type_evars_impls : ?program_mode:bool -> env -> evar_map ->
   ?impls:internalization_env -> constr_expr ->
   evar_map * (types * Impargs.manual_implicits)
 
@@ -158,7 +158,7 @@ val interp_binder_evars : env -> evar_map -> Name.t -> constr_expr -> evar_map *
 (** Interpret contexts: returns extended env and context *)
 
 val interp_context_evars :
-  ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
+  ?program_mode:bool -> ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int ->
   env -> evar_map -> local_binder_expr list ->
   evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 55bfa3cbde4f..29406ef275f5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -107,12 +107,6 @@ let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
 
-(** [program_mode] tells that Program mode has been activated, either
-    globally via [Set Program] or locally via the Program command prefix. *)
-
-let program_mode = ref false
-let is_program_mode () = !program_mode
-
 let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
diff --git a/lib/flags.mli b/lib/flags.mli
index 7336b9beaf7b..b9c5e20f474f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -77,10 +77,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
-(* Miscellaneus flags for vernac *)
-val program_mode : bool ref
-val is_program_mode : unit -> bool
-
 (** Global polymorphic inductive cumulativity flag. *)
 val make_polymorphic_inductive_cumulativity : bool -> unit
 val is_polymorphic_inductive_cumulativity : unit -> bool
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 6f9384941b9b..d06a2419696c 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -40,7 +40,7 @@ let start_deriving f suchthat lemma =
         let f_type = EConstr.Unsafe.to_constr f_type in
         let ef = EConstr.Unsafe.to_constr ef in
         let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
-        let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in
+        let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
         TCons ( env' , sigma , suchthat , (fun sigma _ ->
         TNil sigma))))))
     in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d9b0330e2bce..42dc66dcf461 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -166,7 +166,7 @@ let build_newrecursive
         let arityc = Constrexpr_ops.mkCProdN bl arityc in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
         let evd = Evd.from_env env0 in
-        let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in
+        let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in
         let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in
         let open Context.Named.Declaration in
         (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls))
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1b5286dce481..0c97f9f37381 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1518,10 +1518,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let open CVars in
   let env = Global.env() in
   let evd = Evd.from_env env in
-  let evd, function_type = interp_type_evars env evd type_of_f in
+  let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in
   let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
-  let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
+  let evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in
   let evd = Evd.minimize_universes evd in
   let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
   let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 47f593ff3ef1..ffd8b71e5d77 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -50,7 +50,8 @@ let with_delayed_uconstr ist c tac =
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true
+    expand_evars = true;
+    program_mode = false;
  } in
   let c = Tacinterp.type_uconstr ~flags ist c in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -344,7 +345,9 @@ let constr_flags () = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
   Pretyping.fail_evar = false;
-  Pretyping.expand_evars = true }
+  Pretyping.expand_evars = true;
+  Pretyping.program_mode = false;
+}
 
 let refine_tac ist simple with_classes c =
   Proofview.Goal.enter begin fun gl ->
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 7be8f67616b6..663537f3e806 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -56,7 +56,8 @@ let eval_uconstrs ist cs =
     Pretyping.use_typeclasses = false;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true
+    expand_evars = true;
+    program_mode = false;
   } in
   let map c env sigma = c env sigma in
   List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 3e7479903a76..525ff7fd0f6c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -544,7 +544,9 @@ let constr_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
   fail_evar = true;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 (* Interprets a constr; expects evars to be solved *)
 let interp_constr_gen kind ist env sigma c =
@@ -558,19 +560,25 @@ let open_constr_use_classes_flags () = {
   use_typeclasses = true;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let open_constr_no_classes_flags () = {
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let pure_open_constr_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = false }
+  expand_evars = false;
+  program_mode = false;
+}
 
 (* Interprets an open constr *)
 let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index c3b9bde9b833..0961edb6cb56 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -243,7 +243,9 @@ let interp_refine ist gl rc =
     Pretyping.use_typeclasses = true;
     solve_unification_constraints = true;
     fail_evar = false;
-    expand_evars = true }
+    expand_evars = true;
+    program_mode = false;
+  }
   in
   let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in
 (*   ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 62c27297f3b7..ed7c3d6770ea 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -378,11 +378,11 @@ let is_patvar pat =
   | PatVar _ -> true
   | _ -> false
 
-let coerce_row typing_fun env sigma pats (tomatch,(na,indopt)) =
+let coerce_row ~program_mode typing_fun env sigma pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
   let sigma, tycon, realnames = find_tomatch_tycon !!env sigma loc indopt in
   let sigma, j = typing_fun tycon env sigma tomatch in
-  let sigma, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) !!env sigma j in
+  let sigma, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) ~program_mode !!env sigma j in
   let typ = nf_evar sigma j.uj_type in
   let env = make_return_predicate_ltac_lvar env sigma na tomatch j.uj_val in
   let sigma, t =
@@ -395,12 +395,12 @@ let coerce_row typing_fun env sigma pats (tomatch,(na,indopt)) =
   in
   ((env, sigma), (j.uj_val,t))
 
-let coerce_to_indtype typing_fun env sigma matx tomatchl =
+let coerce_to_indtype ~program_mode typing_fun env sigma matx tomatchl =
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
     | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
     | m -> m in
-  let (env, sigma), tms = List.fold_left2_map (fun (env, sigma) -> coerce_row typing_fun env sigma) (env, sigma) matx' tomatchl in
+  let (env, sigma), tms = List.fold_left2_map (fun (env, sigma) -> coerce_row ~program_mode typing_fun env sigma) (env, sigma) matx' tomatchl in
   env, sigma, tms
 
 (************************************************************************)
@@ -410,7 +410,7 @@ let mkExistential ?(src=(Loc.tag Evar_kinds.InternalHole)) env sigma =
   let sigma, (e, u) = Evarutil.new_type_evar env sigma ~src:src univ_flexible_alg in
   sigma, e
 
-let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) =
+let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
   (* In practice, we coerce the term to match if it is not already an
@@ -435,7 +435,7 @@ let adjust_tomatch_to_pattern sigma pb ((current,typ),deps,dep) =
                 | None -> sigma, current
                 | Some sigma -> sigma, current
 	      else
-                let sigma, j = Coercion.inh_conv_coerce_to true !!(pb.env) sigma (make_judge current typ) indt in
+                let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
                 sigma, j.uj_val
             in
             sigma, (current, try_find_ind !!(pb.env) sigma indt names))
@@ -468,10 +468,11 @@ let remove_current_pattern eqn =
 	    alias_stack = alias_of_pat pat :: eqn.alias_stack }
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
-let push_current_pattern sigma (cur,ty) eqn =
+let push_current_pattern ~program_mode sigma (cur,ty) eqn =
+  let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
   match eqn.patterns with
     | pat::pats ->
-        let _,rhs_env = push_rel sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
+        let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
 	{ eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
 	    patterns = pats }
@@ -562,16 +563,17 @@ let occur_in_rhs na rhs =
     | Name id -> Id.Set.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn pat = match DAst.get pat with
-  | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
+  | PatVar name -> occur_in_rhs name eqn.rhs
   | PatCstr _ -> true
 
-let mk_dep_patt_row (pats,_,eqn) =
-  List.map (is_dep_patt_in eqn) pats
+let mk_dep_patt_row ~program_mode (pats,_,eqn) =
+  if program_mode then List.map (fun _ -> true) pats
+  else List.map (is_dep_patt_in eqn) pats
 
-let dependencies_in_pure_rhs nargs eqns =
+let dependencies_in_pure_rhs ~program_mode nargs eqns =
   if List.is_empty eqns then
-    List.make nargs (not (Flags.is_program_mode ()))  (* Only "_" patts *) else
-  let deps_rows = List.map mk_dep_patt_row eqns in
+    List.make nargs (not program_mode)  (* Only "_" patts *) else
+  let deps_rows = List.map (mk_dep_patt_row ~program_mode) eqns in
   let deps_columns = matrix_transpose deps_rows in
   List.map (List.exists (fun x -> x)) deps_columns
 
@@ -585,10 +587,10 @@ let rec dep_in_tomatch sigma n = function
   | Abstract (_,d) :: l -> RelDecl.exists (fun c -> not (noccurn sigma n c)) d || dep_in_tomatch sigma (n+1) l
   | [] -> false
 
-let dependencies_in_rhs sigma nargs current tms eqns =
+let dependencies_in_rhs ~program_mode sigma nargs current tms eqns =
   match EConstr.kind sigma current with
   | Rel n when dep_in_tomatch sigma n tms -> List.make nargs true
-  | _ -> dependencies_in_pure_rhs nargs eqns
+  | _ -> dependencies_in_pure_rhs ~program_mode nargs eqns
 
 (* Computing the matrix of dependencies *)
 
@@ -788,9 +790,9 @@ let recover_and_adjust_alias_names (_,avoid) names sign =
   in
   List.split (aux (names,sign))
 
-let push_rels_eqn sigma sign eqn =
+let push_rels_eqn ~hypnaming sigma sign eqn =
   {eqn with
-     rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } }
+     rhs = {eqn.rhs with rhs_env = snd (push_rel_context ~hypnaming sigma sign eqn.rhs.rhs_env) } }
 
 let push_rels_eqn_with_names sigma sign eqn =
   let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
@@ -798,12 +800,12 @@ let push_rels_eqn_with_names sigma sign eqn =
   let sign = recover_initial_subpattern_names subpatnames sign in
   push_rels_eqn sigma sign eqn
 
-let push_generalized_decl_eqn env sigma n decl eqn =
+let push_generalized_decl_eqn ~hypnaming env sigma n decl eqn =
   match RelDecl.get_name decl with
   | Anonymous ->
-      push_rels_eqn sigma [decl] eqn
+      push_rels_eqn ~hypnaming sigma [decl] eqn
   | Name _ ->
-      push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
+      push_rels_eqn ~hypnaming sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
 
 let drop_alias_eqn eqn =
   { eqn with alias_stack = List.tl eqn.alias_stack }
@@ -1266,7 +1268,7 @@ let build_leaf sigma pb =
 (* Build the sub-pattern-matching problem for a given branch "C x1..xn as x" *)
 (* spiwack: the [initial] argument keeps track whether the branch is a
    toplevel branch ([true]) or a deep one ([false]). *)
-let build_branch initial current realargs deps (realnames,curname) sigma pb arsign eqns const_info =
+let build_branch ~program_mode initial current realargs deps (realnames,curname) sigma pb arsign eqns const_info =
   (* We remember that we descend through constructor C *)
   let history =
     push_history_pattern const_info.cs_nargs (fst const_info.cs_cstr) pb.history in
@@ -1296,7 +1298,8 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
   let typs' =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
 
-  let typs,extenv = push_rel_context sigma typs pb.env in
+  let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+  let typs,extenv = push_rel_context ~hypnaming sigma typs pb.env in
 
   let typs' =
     List.map (fun (c,d) ->
@@ -1306,7 +1309,7 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
   (* generalization *)
   let dep_sign =
     find_dependencies_signature sigma
-      (dependencies_in_rhs sigma const_info.cs_nargs current pb.tomatch eqns)
+      (dependencies_in_rhs ~program_mode sigma const_info.cs_nargs current pb.tomatch eqns)
       (List.rev typs') in
 
   (* The dependent term to subst in the types of the remaining UnPushed
@@ -1375,7 +1378,7 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
       tomatch = tomatch;
       pred = pred;
       history = history;
-      mat = List.map (push_rels_eqn_with_names sigma typs) submat }
+      mat = List.map (push_rels_eqn_with_names ~hypnaming sigma typs) submat }
 
 (**********************************************************************
  INVARIANT:
@@ -1390,181 +1393,187 @@ let build_branch initial current realargs deps (realnames,curname) sigma pb arsi
 
 (**********************************************************************)
 (* Main compiling descent *)
-let rec compile sigma pb =
-  match pb.tomatch with
-    | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
-    | Alias (initial,x) :: rest -> compile_alias initial sigma pb x rest
-    | NonDepAlias :: rest -> compile_non_dep_alias sigma pb rest
-    | Abstract (i,d) :: rest -> compile_generalization sigma pb i d rest
-    | [] -> build_leaf sigma pb
+let compile ~program_mode sigma pb =
+  let rec compile sigma pb =
+    match pb.tomatch with
+      | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
+      | Alias (initial,x) :: rest -> compile_alias initial sigma pb x rest
+      | NonDepAlias :: rest -> compile_non_dep_alias sigma pb rest
+      | Abstract (i,d) :: rest -> compile_generalization sigma pb i d rest
+      | [] -> build_leaf sigma pb
 
 (* Case splitting *)
-and match_current sigma pb (initial,tomatch) =
-  let sigma, tm = adjust_tomatch_to_pattern sigma pb tomatch in
-  let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
-  let ((current,typ),deps,dep) = tomatch in
-  match typ with
-    | NotInd (_,typ) ->
-        check_all_variables !!(pb.env) sigma typ pb.mat;
-        compile_all_variables initial tomatch sigma pb
-    | IsInd (_,(IndType(indf,realargs) as indt),names) ->
+  and match_current sigma pb (initial,tomatch) =
+    let sigma, tm = adjust_tomatch_to_pattern ~program_mode sigma pb tomatch in
+    let pb,tomatch = adjust_predicate_from_tomatch tomatch tm pb in
+    let ((current,typ),deps,dep) = tomatch in
+    match typ with
+      | NotInd (_,typ) ->
+          check_all_variables !!(pb.env) sigma typ pb.mat;
+          compile_all_variables initial tomatch sigma pb
+      | IsInd (_,(IndType(indf,realargs) as indt),names) ->
 	let mind,_ = dest_ind_family indf in
-        let mind = Tacred.check_privacy !!(pb.env) mind in
-        let cstrs = get_constructors !!(pb.env) indf in
-        let arsign, _ = get_arity !!(pb.env) indf in
+          let mind = Tacred.check_privacy !!(pb.env) mind in
+          let cstrs = get_constructors !!(pb.env) indf in
+          let arsign, _ = get_arity !!(pb.env) indf in
 	let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
-        let no_cstr = Int.equal (Array.length cstrs) 0 in
+          let no_cstr = Int.equal (Array.length cstrs) 0 in
 	if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
-          compile_all_variables initial tomatch sigma pb
+            compile_all_variables initial tomatch sigma pb
 	else
 	  (* We generalize over terms depending on current term to match *)
-          let pb,deps = generalize_problem (names,dep) sigma pb deps in
+            let pb,deps = generalize_problem (names,dep) sigma pb deps in
 
 	  (* We compile branches *)
-          let fold_br sigma eqn cstr =
-            compile_branch initial current realargs (names,dep) deps sigma pb arsign eqn cstr
-          in
-          let sigma, brvals = Array.fold_left2_map fold_br sigma eqns cstrs in
+            let fold_br sigma eqn cstr =
+              compile_branch initial current realargs (names,dep) deps sigma pb arsign eqn cstr
+            in
+            let sigma, brvals = Array.fold_left2_map fold_br sigma eqns cstrs in
 	  (* We build the (elementary) case analysis *)
-          let depstocheck = current::binding_vars_of_inductive sigma typ in
-          let brvals,tomatch,pred,inst =
-            postprocess_dependencies sigma depstocheck
-              brvals pb.tomatch pb.pred deps cstrs in
-          let brvals = Array.map (fun (sign,body) ->
-            it_mkLambda_or_LetIn body sign) brvals in
+            let depstocheck = current::binding_vars_of_inductive sigma typ in
+            let brvals,tomatch,pred,inst =
+              postprocess_dependencies sigma depstocheck
+                brvals pb.tomatch pb.pred deps cstrs in
+            let brvals = Array.map (fun (sign,body) ->
+              it_mkLambda_or_LetIn body sign) brvals in
 	  let (pred,typ) =
-            find_predicate pb.caseloc pb.env sigma
+              find_predicate pb.caseloc pb.env sigma
 	      pred current indt (names,dep) tomatch in
-          let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
-          let pred = nf_betaiota !!(pb.env) sigma pred in
+            let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
+            let pred = nf_betaiota !!(pb.env) sigma pred in
 	  let case =
-            make_case_or_project !!(pb.env) sigma indf ci pred current brvals
+              make_case_or_project !!(pb.env) sigma indf ci pred current brvals
 	  in
-          let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
-          Typing.check_allowed_sort !!(pb.env) sigma mind current pred;
-          sigma, { uj_val = applist (case, inst);
-            uj_type = prod_applist sigma typ inst }
-
-
-(* Building the sub-problem when all patterns are variables. Case
-   where [current] is an intially pushed term. *)
-and shift_problem ((current,t),_,na) sigma pb =
-  let ty = type_of_tomatch t in
-  let tomatch = lift_tomatch_stack 1 pb.tomatch in
-  let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
-  let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
-  let pb =
-    { pb with
-       env = snd (push_rel sigma (LocalDef (na,current,ty)) env);
-       tomatch = tomatch;
-       pred = lift_predicate 1 pred tomatch;
-       history = pop_history pb.history;
-       mat = List.map (push_current_pattern sigma (current,ty)) pb.mat } in
-  let sigma, j = compile sigma pb in
-  sigma, { uj_val = subst1 current j.uj_val;
-    uj_type = subst1 current j.uj_type }
-
-(* Building the sub-problem when all patterns are variables,
-   non-initial case. Variables which appear as subterms of constructor
-   are already introduced in the context, we avoid creating aliases to
-   themselves by treating this case specially. *)
-and pop_problem ((current,t),_,na) sigma pb =
-  let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
-  let pb =
-    { pb with
-       pred = pred;
-       history = pop_history pb.history;
-       mat = List.map push_noalias_current_pattern pb.mat } in
-  compile sigma pb
+            let sigma, _ = Typing.type_of !!(pb.env) sigma pred in
+            Typing.check_allowed_sort !!(pb.env) sigma mind current pred;
+            sigma, { uj_val = applist (case, inst);
+              uj_type = prod_applist sigma typ inst }
+
+
+  (* Building the sub-problem when all patterns are variables. Case
+     where [current] is an intially pushed term. *)
+  and shift_problem ((current,t),_,na) sigma pb =
+    let ty = type_of_tomatch t in
+    let tomatch = lift_tomatch_stack 1 pb.tomatch in
+    let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+    let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let pb =
+      { pb with
+         env = snd (push_rel ~hypnaming sigma (LocalDef (na,current,ty)) env);
+         tomatch = tomatch;
+         pred = lift_predicate 1 pred tomatch;
+         history = pop_history pb.history;
+         mat = List.map (push_current_pattern ~program_mode sigma (current,ty)) pb.mat } in
+    let sigma, j = compile sigma pb in
+    sigma, { uj_val = subst1 current j.uj_val;
+      uj_type = subst1 current j.uj_type }
+
+  (* Building the sub-problem when all patterns are variables,
+     non-initial case. Variables which appear as subterms of constructor
+     are already introduced in the context, we avoid creating aliases to
+     themselves by treating this case specially. *)
+  and pop_problem ((current,t),_,na) sigma pb =
+    let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+    let pb =
+      { pb with
+         pred = pred;
+         history = pop_history pb.history;
+         mat = List.map push_noalias_current_pattern pb.mat } in
+    compile sigma pb
 
-(* Building the sub-problem when all patterns are variables. *)
-and compile_all_variables initial cur sigma pb =
-  if initial then shift_problem cur sigma pb
-  else pop_problem cur sigma pb
+  (* Building the sub-problem when all patterns are variables. *)
+  and compile_all_variables initial cur sigma pb =
+    if initial then shift_problem cur sigma pb
+    else pop_problem cur sigma pb
 
-(* Building the sub-problem when all patterns are variables *)
-and compile_branch initial current realargs names deps sigma pb arsign eqns cstr =
-  let sigma, sign, pb = build_branch initial current realargs deps names sigma pb arsign eqns cstr in
-  let sigma, j = compile sigma pb in
-  sigma, (sign, j.uj_val)
+  (* Building the sub-problem when all patterns are variables *)
+  and compile_branch initial current realargs names deps sigma pb arsign eqns cstr =
+    let sigma, sign, pb = build_branch ~program_mode initial current realargs deps names sigma pb arsign eqns cstr in
+    let sigma, j = compile sigma pb in
+    sigma, (sign, j.uj_val)
 
-(* Abstract over a declaration before continuing splitting *)
-and compile_generalization sigma pb i d rest =
-  let pb =
-    { pb with
-       env = snd (push_rel sigma d pb.env);
-       tomatch = rest;
-       mat = List.map (push_generalized_decl_eqn pb.env sigma i d) pb.mat } in
-  let sigma, j = compile sigma pb in
-  sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
-    uj_type = mkProd_wo_LetIn d j.uj_type }
-
-(* spiwack: the [initial] argument keeps track whether the alias has
-   been introduced by a toplevel branch ([true]) or a deep one
-   ([false]). *)
-and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest =
-  let f c t =
-    let alias = LocalDef (na,c,t) in
+  (* Abstract over a declaration before continuing splitting *)
+  and compile_generalization sigma pb i d rest =
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let pb =
       { pb with
-         env = snd (push_rel sigma alias pb.env);
-         tomatch = lift_tomatch_stack 1 rest;
-         pred = lift_predicate 1 pb.pred pb.tomatch;
-         history = pop_history_pattern pb.history;
-         mat = List.map (push_alias_eqn sigma alias) pb.mat } in
+         env = snd (push_rel ~hypnaming sigma d pb.env);
+         tomatch = rest;
+         mat = List.map (push_generalized_decl_eqn ~hypnaming pb.env sigma i d) pb.mat } in
     let sigma, j = compile sigma pb in
-    sigma, { uj_val =
-        if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
-          subst1 c j.uj_val
-        else
-          mkLetIn (na,c,t,j.uj_val);
-      uj_type = subst1 c j.uj_type } in
-  (* spiwack: when an alias appears on a deep branch, its non-expanded
-     form is automatically a variable of the same name. We avoid
-     introducing such superfluous aliases so that refines are elegant. *)
-  let just_pop sigma =
+    sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
+      uj_type = mkProd_wo_LetIn d j.uj_type }
+
+  (* spiwack: the [initial] argument keeps track whether the alias has
+     been introduced by a toplevel branch ([true]) or a deep one
+     ([false]). *)
+  and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest =
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let f c t =
+      let alias = LocalDef (na,c,t) in
+      let pb =
+        { pb with
+           env = snd (push_rel ~hypnaming sigma alias pb.env);
+           tomatch = lift_tomatch_stack 1 rest;
+           pred = lift_predicate 1 pb.pred pb.tomatch;
+           history = pop_history_pattern pb.history;
+           mat = List.map (push_alias_eqn ~hypnaming sigma alias) pb.mat } in
+      let sigma, j = compile sigma pb in
+      sigma, { uj_val =
+          if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
+            subst1 c j.uj_val
+          else
+            mkLetIn (na,c,t,j.uj_val);
+        uj_type = subst1 c j.uj_type } in
+    (* spiwack: when an alias appears on a deep branch, its non-expanded
+       form is automatically a variable of the same name. We avoid
+       introducing such superfluous aliases so that refines are elegant. *)
+    let just_pop sigma =
+      let pb =
+        { pb with
+          tomatch = rest;
+          history = pop_history_pattern pb.history;
+          mat = List.map drop_alias_eqn pb.mat } in
+      compile sigma pb
+    in
+    (* If the "match" was orginally over a variable, as in "match x with
+       O => true | n => n end", we give preference to non-expansion in
+       the default clause (i.e. "match x with O => true | n => n end"
+       rather than "match x with O => true | S p => S p end";
+       computationally, this avoids reallocating constructors in cbv
+       evaluation; the drawback is that it might duplicate the instances
+       of the term to match when the corresponding variable is
+       substituted by a non-evaluated expression *)
+    if not program_mode && (isRel sigma orig || isVar sigma orig) then
+      (* Try to compile first using non expanded alias *)
+      try
+        if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
+        else just_pop sigma
+      with e when precatchable_exception e ->
+      (* Try then to compile using expanded alias *)
+      (* Could be needed in case of dependent return clause *)
+      f expanded expanded_typ
+    else
+      (* Try to compile first using expanded alias *)
+      try f expanded expanded_typ
+      with e when precatchable_exception e ->
+      (* Try then to compile using non expanded alias *)
+      (* Could be needed in case of a recursive call which requires to
+         be on a variable for size reasons *)
+      if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
+      else just_pop sigma
+
+
+  (* Remember that a non-trivial pattern has been consumed *)
+  and compile_non_dep_alias sigma pb rest =
     let pb =
       { pb with
-        tomatch = rest;
-        history = pop_history_pattern pb.history;
-        mat = List.map drop_alias_eqn pb.mat } in
+         tomatch = rest;
+         history = pop_history_pattern pb.history;
+         mat = List.map drop_alias_eqn pb.mat } in
     compile sigma pb
   in
-  (* If the "match" was orginally over a variable, as in "match x with
-     O => true | n => n end", we give preference to non-expansion in
-     the default clause (i.e. "match x with O => true | n => n end"
-     rather than "match x with O => true | S p => S p end";
-     computationally, this avoids reallocating constructors in cbv
-     evaluation; the drawback is that it might duplicate the instances
-     of the term to match when the corresponding variable is
-     substituted by a non-evaluated expression *)
-  if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
-    (* Try to compile first using non expanded alias *)
-    try
-      if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
-      else just_pop sigma
-    with e when precatchable_exception e ->
-    (* Try then to compile using expanded alias *)
-    (* Could be needed in case of dependent return clause *)
-    f expanded expanded_typ
-  else
-    (* Try to compile first using expanded alias *)
-    try f expanded expanded_typ
-    with e when precatchable_exception e ->
-    (* Try then to compile using non expanded alias *)
-    (* Could be needed in case of a recursive call which requires to
-       be on a variable for size reasons *)
-    if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
-    else just_pop sigma
-
-
-(* Remember that a non-trivial pattern has been consumed *)
-and compile_non_dep_alias sigma pb rest =
-  let pb =
-    { pb with
-       tomatch = rest;
-       history = pop_history_pattern pb.history;
-       mat = List.map drop_alias_eqn pb.mat } in
   compile sigma pb
 
 (* pour les alias des initiaux, enrichir les env de ce qu'il faut et
@@ -1650,7 +1659,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
   (subst0, t0)
 
 let push_binder sigma d (k,env,subst) =
-  (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+  (k+1,snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
 
 let rec list_assoc_in_triple x = function
     [] -> raise Not_found
@@ -1771,7 +1780,7 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
  * further explanations
  *)
 
-let build_inversion_problem loc env sigma tms t =
+let build_inversion_problem ~program_mode loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in
     DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
@@ -1796,13 +1805,13 @@ let build_inversion_problem loc env sigma tms t =
         let patl = pat :: List.rev patl in
         let patl,sign = recover_and_adjust_alias_names acc patl sign in
 	let p = List.length patl in
-        let _,env' = push_rel_context sigma sign env in
+        let _,env' = push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma sign env in
 	let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
 	List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let d = LocalAssum (alias_of_pat pat,typ) in
-      let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in
+      let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
   let avoid0 = GlobEnv.vars_of_env env in
   (* [patl] is a list of patterns revealing the substructure of
@@ -1820,7 +1829,7 @@ let build_inversion_problem loc env sigma tms t =
   let decls =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
 
-  let _,pb_env = push_rel_context sigma sign env in
+  let _,pb_env = push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma sign env in
   let decls =
     List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in
 
@@ -1881,7 +1890,7 @@ let build_inversion_problem loc env sigma tms t =
       caseloc   = loc;
       casestyle = RegularStyle;
       typing_function = build_tycon ?loc env pb_env s subst} in
-  let sigma, j = compile sigma pb in
+  let sigma, j = compile ~program_mode sigma pb in
   (sigma, j.uj_val)
 
 (* Here, [pred] is assumed to be in the context built from all *)
@@ -1934,9 +1943,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
     | _ -> assert false
   in List.rev (buildrec 0 (tomatchl,tmsign))
 
-let inh_conv_coerce_to_tycon ?loc env sigma j tycon =
+let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon =
   match tycon with
-    | Some p -> Coercion.inh_conv_coerce_to ?loc true env sigma j p
+    | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma j p
     | None -> sigma, j
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
@@ -1953,7 +1962,7 @@ let dependent_rel_or_var sigma tm c =
   | Var id -> Termops.local_occur_var sigma id c
   | _ -> assert false
 
-let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
+let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
   let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
@@ -2006,7 +2015,8 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   in
   assert (len == 0);
   let p = predicate 0 c in
-  let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in
+  let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+  let arsign,env' = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in
   try let sigma' = fst (Typing.type_of !!env' sigma p) in
         Some (sigma', p, arsign)
   with e when precatchable_exception e -> None
@@ -2019,7 +2029,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * Each matched term is independently considered dependent or not.
  *)
 
-let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
+let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign tycon pred =
   let refresh_tycon sigma t =
     (* If we put the typing constraint in the term, it has to be
        refreshed to preserve the invariant that no algebraic universe
@@ -2041,10 +2051,10 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
              sigma, t in
         (* First strategy: we build an "inversion" predicate, also replacing the *)
         (* dependencies with existential variables *)
-        let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+        let sigma1,pred1 = build_inversion_problem loc ~program_mode env sigma tomatchs t in
         (* Optional second strategy: we abstract the tycon wrt to the dependencies *)
         let p2 =
-          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+          prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in
         (* Third strategy: we take the type constraint as it is; of course we could *)
         (* need something inbetween, abstracting some but not all of the dependencies *)
         (* the "inversion" strategy deals with that but unification may not be *)
@@ -2060,7 +2070,7 @@ let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
     (* Some type annotation *)
     | Some rtntyp ->
       (* We extract the signature of the arity *)
-      let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
+      let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma) arsign env in
       let sigma, newt = new_sort_variable univ_flexible sigma in
       let sigma, predcclj = typing_fun (mk_tycon (mkSort newt)) envar sigma rtntyp in
       let predccl = nf_evar sigma predcclj.uj_val in
@@ -2320,7 +2330,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
 	 in
          let sigma, ineqs = build_ineqs sigma prevpatterns pats signlen in
          let rhs_rels' = rels_of_patsign sigma rhs_rels in
-         let _signenv,_ = push_rel_context sigma rhs_rels' env in
+         let _signenv,_ = push_rel_context ~hypnaming:ProgramNaming sigma rhs_rels' env in
 	 let arity =
 	   let args, nargs =
 	     List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
@@ -2340,7 +2350,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
            let eqs_rels, arity = decompose_prod_n_assum sigma neqs arity in
 	     eqs_rels @ neqs_rels @ rhs_rels', arity
 	 in
-         let _,rhs_env = push_rel_context sigma rhs_rels' env in
+         let _,rhs_env = push_rel_context ~hypnaming:ProgramNaming sigma rhs_rels' env in
          let sigma, j = typing_fun (mk_tycon tycon) rhs_env sigma eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
@@ -2518,10 +2528,10 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let env, sigma, tomatchs = coerce_to_indtype typing_function env sigma matx tomatchl in
+  let env, sigma, tomatchs = coerce_to_indtype ~program_mode:true typing_function env sigma matx tomatchl in
   let tycon = valcon_of_tycon tycon in
   let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env sigma tomatchs tycon in
-  let _,env = push_rel_context sigma tomatchs_lets env in
+  let _,env = push_rel_context ~hypnaming:ProgramNaming sigma tomatchs_lets env in
   let len = List.length eqns in
   let sigma, sign, allnames, signlen, eqs, neqs, args =
     (* The arity signature *)
@@ -2540,7 +2550,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
       sigma, ev, lift nar ev
     | Some t ->
         let sigma, pred =
-          match prepare_predicate_from_arsign_tycon env sigma loc tomatchs sign t with
+          match prepare_predicate_from_arsign_tycon ~program_mode:true env sigma loc tomatchs sign t with
           | Some (evd, pred, arsign) -> evd, pred
           | None -> sigma, lift nar t
         in
@@ -2557,7 +2567,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
   in
   let matx = List.rev matx in
   let _ = assert (Int.equal len (List.length lets)) in
-  let _,env = push_rel_context sigma lets env in
+  let _,env = push_rel_context ~hypnaming:ProgramNaming sigma lets env in
   let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
   let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
   let args = List.rev_map (lift len) args in
@@ -2604,7 +2614,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
       casestyle= style;
       typing_function = typing_function } in
 
-  let sigma, j = compile sigma pb in
+  let sigma, j = compile ~program_mode:true sigma pb in
     (* We check for unused patterns *)
     List.iter (check_unused_pattern !!env) matx;
     let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
@@ -2617,8 +2627,8 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
-let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, eqns) =
-  if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
+let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predopt, tomatchl, eqns) =
+  if predopt == None && program_mode && Program.is_program_cases () then
     compile_program_cases ?loc style (typing_fun, sigma)
       tycon env (predopt, tomatchl, eqns)
   else
@@ -2628,13 +2638,13 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
 
   (* We build the vector of terms to match consistently with the *)
   (* constructors found in patterns *)
-  let predenv, sigma, tomatchs = coerce_to_indtype typing_fun env sigma matx tomatchl in
+  let predenv, sigma, tomatchs = coerce_to_indtype ~program_mode typing_fun env sigma matx tomatchl in
 
   (* If an elimination predicate is provided, we check it is compatible
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
   let arsign = extract_arity_signature !!env tomatchs tomatchl in
-  let preds = prepare_predicate ?loc typing_fun predenv sigma tomatchs arsign tycon predopt in
+  let preds = prepare_predicate ?loc ~program_mode typing_fun predenv sigma tomatchs arsign tycon predopt in
 
   let compile_for_one_predicate (sigma,nal,pred) =
     (* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2679,10 +2689,10 @@ let compile_cases ?loc style (typing_fun, sigma) tycon env (predopt, tomatchl, e
 	casestyle = style;
 	typing_function = typing_fun } in
 
-    let sigma, j = compile sigma pb in
+    let sigma, j = compile ~program_mode sigma pb in
 
     (* We coerce to the tycon (if an elim predicate was provided) *)
-    inh_conv_coerce_to_tycon ?loc !!env sigma j tycon
+    inh_conv_coerce_to_tycon ?loc ~program_mode !!env sigma j tycon
   in
 
   (* Return the term compiled with the first possible elimination  *)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 36cfa0a70dd1..b0349a3d0537 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -40,7 +40,7 @@ val irrefutable : env -> cases_pattern -> bool
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
-  ?loc:Loc.t -> case_style ->
+  ?loc:Loc.t -> program_mode:bool -> case_style ->
   (type_constraint -> GlobEnv.t -> evar_map -> glob_constr -> evar_map * unsafe_judgment) * evar_map ->
   type_constraint ->
   GlobEnv.t -> glob_constr option * tomatch_tuples * cases_clauses ->
@@ -111,9 +111,9 @@ type 'a pattern_matching_problem =
       casestyle : case_style;
       typing_function: type_constraint -> GlobEnv.t -> evar_map -> 'a option -> evar_map * unsafe_judgment }
 
-val compile : evar_map -> 'a pattern_matching_problem -> evar_map * unsafe_judgment
+val compile : program_mode:bool -> evar_map -> 'a pattern_matching_problem -> evar_map * unsafe_judgment
 
-val prepare_predicate : ?loc:Loc.t ->
+val prepare_predicate : ?loc:Loc.t -> program_mode:bool ->
            (type_constraint ->
             GlobEnv.t -> Evd.evar_map -> glob_constr -> Evd.evar_map * unsafe_judgment) ->
            GlobEnv.t ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 4d1d405bd7c4..9e93c470b169 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -393,7 +393,7 @@ let apply_coercion env sigma p hj typ_cl =
   with NoCoercion as e -> raise e
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
-let inh_app_fun_core env evd j =
+let inh_app_fun_core ~program_mode env evd j =
   let t = whd_all env evd j.uj_type in
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
@@ -404,25 +404,25 @@ let inh_app_fun_core env evd j =
       	try let t,p =
 	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
-	with Not_found | NoCoercion ->
-          if Flags.is_program_mode () then
-	  try
-	    let evdref = ref evd in
-	    let coercef, t = mu env evdref t in
-	    let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
-	      (!evdref, res)
-	  with NoSubtacCoercion | NoCoercion ->
-	    (evd,j)
-          else raise NoCoercion
+       with Not_found | NoCoercion ->
+         if program_mode then
+           try
+             let evdref = ref evd in
+             let coercef, t = mu env evdref t in
+             let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
+             (!evdref, res)
+           with NoSubtacCoercion | NoCoercion ->
+             (evd,j)
+         else raise NoCoercion
 
 (* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
-let inh_app_fun resolve_tc env evd j =
-  try inh_app_fun_core env evd j
+let inh_app_fun ~program_mode resolve_tc env evd j =
+  try inh_app_fun_core ~program_mode env evd j
   with
   | NoCoercion when not resolve_tc
     || not (get_use_typeclasses_for_conversion ()) -> (evd, j)
   | NoCoercion ->
-    try inh_app_fun_core env (saturate_evd env evd) j
+    try inh_app_fun_core ~program_mode env (saturate_evd env evd) j
     with NoCoercion -> (evd, j)
 
 let type_judgment env sigma j =
@@ -449,8 +449,8 @@ let inh_coerce_to_sort ?loc env evd j =
     | _ ->
 	inh_tosort_force ?loc env evd j
 
-let inh_coerce_to_base ?loc env evd j =
-  if Flags.is_program_mode () then
+let inh_coerce_to_base ?loc ~program_mode env evd j =
+  if program_mode then
     let evdref = ref evd in
     let ct, typ' = mu env evdref j.uj_type in
     let res =
@@ -459,8 +459,8 @@ let inh_coerce_to_base ?loc env evd j =
     in !evdref, res
   else (evd, j)
 
-let inh_coerce_to_prod ?loc env evd t =
-  if Flags.is_program_mode () then
+let inh_coerce_to_prod ?loc ~program_mode env evd t =
+  if program_mode then
     let evdref = ref evd in
     let _, typ' = mu env evdref t in
       !evdref, typ'
@@ -520,13 +520,13 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 =
       | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
 
 (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
+let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t =
   let (evd', val') =
     try
       inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
-	if Flags.is_program_mode () then
+        if program_mode then
 	  coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
       with
@@ -545,9 +545,11 @@ let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t =
   let val' = match val' with Some v -> v | None -> assert(false) in
     (evd',{ uj_val = val'; uj_type = t })
 
-let inh_conv_coerce_to ?loc resolve_tc = inh_conv_coerce_to_gen ?loc resolve_tc false
+let inh_conv_coerce_to ?loc ~program_mode resolve_tc =
+  inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false
 
-let inh_conv_coerce_rigid_to ?loc resolve_tc = inh_conv_coerce_to_gen resolve_tc ?loc true
+let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc =
+  inh_conv_coerce_to_gen ~program_mode resolve_tc ?loc true
 
 let inh_conv_coerces_to ?loc env evd t t' =
   try
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 6cfd958b4636..a9413911259b 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -21,7 +21,7 @@ open Glob_term
     type a product; it returns [j] if no coercion is applicable.
     resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
-val inh_app_fun : bool ->
+val inh_app_fun : program_mode:bool -> bool ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
 (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
@@ -33,11 +33,11 @@ val inh_coerce_to_sort : ?loc:Loc.t ->
 (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
     inserts a coercion into [j], if needed, in such a way it gets as
     type its base type (the notion depends on the coercion system) *)
-val inh_coerce_to_base : ?loc:Loc.t ->
+val inh_coerce_to_base : ?loc:Loc.t -> program_mode:bool ->
   env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
 
 (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
-val inh_coerce_to_prod : ?loc:Loc.t ->
+val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool ->
   env -> evar_map -> types -> evar_map * types
 
 (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an 
@@ -45,10 +45,10 @@ val inh_coerce_to_prod : ?loc:Loc.t ->
     a way [t] and [j.uj_type] are convertible; it fails if no coercion is
     applicable. resolve_tc=false disables resolving type classes (as the last
     resort before failing) *)
-val inh_conv_coerce_to : ?loc:Loc.t -> bool ->
+val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
-val inh_conv_coerce_rigid_to : ?loc:Loc.t -> bool ->
+val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool ->
   env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
 (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 49a08afe80dd..d6b204561eaf 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -38,10 +38,10 @@ type t = {
   lvar : ltac_var_map;
 }
 
-let make env sigma lvar =
+let make ~hypnaming env sigma lvar =
   let get_extra env sigma =
     let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
-    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+    Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
       (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
   {
     static_env = env;
@@ -66,32 +66,32 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
 
 let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
 
-let push_rel sigma d env =
+let push_rel ~hypnaming sigma d env =
   let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
   let env = {
     static_env = push_rel d env.static_env;
     renamed_env = push_rel d' env.renamed_env;
-    extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+    extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   d', env
 
-let push_rel_context ?(force_names=false) sigma ctx env =
+let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
   let open Context.Rel.Declaration in
   let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
   let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
   let env = {
     static_env = push_rel_context ctx env.static_env;
     renamed_env = push_rel_context ctx' env.renamed_env;
-    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   ctx', env
 
-let push_rec_types sigma (lna,typarray) env =
+let push_rec_types ~hypnaming sigma (lna,typarray) env =
   let open Context.Rel.Declaration in
   let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
-  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in
   Array.map get_name ctx, env
 
 let new_evar env sigma ?src ?naming typ =
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index e8a2fbdd16a0..63f72e60bdd7 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -13,6 +13,7 @@ open Environ
 open Evd
 open EConstr
 open Ltac_pretype
+open Evarutil
 
 (** To embed constr in glob_constr *)
 
@@ -37,7 +38,7 @@ type t
 
 (** Build a pretyping environment from an ltac environment *)
 
-val make : env -> evar_map -> ltac_var_map -> t
+val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
 
 (** Export the underlying environement *)
 
@@ -47,9 +48,9 @@ val vars_of_env : t -> Id.Set.t
 
 (** Push to the environment, returning the declaration(s) with interpreted names *)
 
-val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
-val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
-val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t
+val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t
 
 (** Declare an evar using renaming information *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 57705fa20991..46e463512d36 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -190,7 +190,8 @@ type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
   fail_evar : bool;
-  expand_evars : bool
+  expand_evars : bool;
+  program_mode : bool;
 }
 
 (* Compute the set of still-undefined initial evars up to restriction
@@ -226,17 +227,17 @@ let frozen_and_pending_holes (sigma, sigma') =
     end in
     FrozenProgress data
 
-let apply_typeclasses env sigma frozen fail_evar =
+let apply_typeclasses ~program_mode env sigma frozen fail_evar =
   let filter_frozen = match frozen with
     | FrozenId map -> fun evk -> Evar.Map.mem evk map
     | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
   in
   let sigma = Typeclasses.resolve_typeclasses
-      ~filter:(if Flags.is_program_mode ()
+      ~filter:(if program_mode
                then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
                else (fun evk evi -> Typeclasses.no_goals evk evi && not (filter_frozen evk)))
       ~split:true ~fail:fail_evar env sigma in
-  let sigma = if Flags.is_program_mode () then (* Try optionally solving the obligations *)
+  let sigma = if program_mode then (* Try optionally solving the obligations *)
       Typeclasses.resolve_typeclasses
         ~filter:(fun evk evi -> Typeclasses.all_evars evk evi && not (filter_frozen evk)) ~split:true ~fail:false env sigma
     else sigma in
@@ -264,9 +265,9 @@ let apply_heuristics env sigma fail_evar =
     let e = CErrors.push e in
     if fail_evar then iraise e else sigma
 
-let check_typeclasses_instances_are_solved env current_sigma frozen =
+let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses env current_sigma frozen true
+  apply_typeclasses ~program_mode env current_sigma frozen true
 
 let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 | FrozenId _ -> ()
@@ -295,18 +296,19 @@ let check_evars env initial_sigma sigma c =
     | _ -> EConstr.iter sigma proc_rec c
   in proc_rec c
 
-let check_evars_are_solved env sigma frozen =
-  let sigma = check_typeclasses_instances_are_solved env sigma frozen in
+let check_evars_are_solved ~program_mode env sigma frozen =
+  let sigma = check_typeclasses_instances_are_solved ~program_mode env sigma frozen in
   check_problems_are_solved env sigma;
   check_extra_evars_are_solved env sigma frozen
 
 (* Try typeclasses, hooks, unification heuristics ... *)
 
 let solve_remaining_evars ?hook flags env ?initial sigma =
+  let program_mode = flags.program_mode in
   let frozen = frozen_and_pending_holes (initial, sigma) in
   let sigma =
     if flags.use_typeclasses
-    then apply_typeclasses env sigma frozen false
+    then apply_typeclasses ~program_mode env sigma frozen false
     else sigma
   in
   let sigma = match hook with
@@ -317,12 +319,12 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
     then apply_heuristics env sigma false
     else sigma
   in
-  if flags.fail_evar then check_evars_are_solved env sigma frozen;
+  if flags.fail_evar then check_evars_are_solved ~program_mode env sigma frozen;
   sigma
 
-let check_evars_are_solved env ?initial current_sigma =
+let check_evars_are_solved ~program_mode env ?initial current_sigma =
   let frozen = frozen_and_pending_holes (initial, current_sigma) in
-  check_evars_are_solved env current_sigma frozen
+  check_evars_are_solved ~program_mode env current_sigma frozen
 
 let process_inference_flags flags env initial (sigma,c,cty) =
   let sigma = solve_remaining_evars flags env ~initial sigma in
@@ -351,10 +353,10 @@ let adjust_evar_source sigma na c =
   | _, _ -> sigma, c
 
 (* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon ?loc resolve_tc env sigma j = function
+let inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc env sigma j = function
   | None -> sigma, j
   | Some t ->
-    Coercion.inh_conv_coerce_to ?loc resolve_tc !!env sigma j t
+    Coercion.inh_conv_coerce_to ?loc ~program_mode resolve_tc !!env sigma j t
 
 let check_instance loc subst = function
   | [] -> ()
@@ -453,20 +455,18 @@ let new_type_evar env sigma loc =
   new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
 
 let mark_obligation_evar sigma k evc =
-  if Flags.is_program_mode () then
-    match k with
-    | Evar_kinds.QuestionMark _
-    | Evar_kinds.ImplicitArg (_, _, false) ->
-      Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
-    | _ -> sigma
-  else sigma
+  match k with
+  | Evar_kinds.QuestionMark _
+  | Evar_kinds.ImplicitArg (_, _, false) ->
+    Evd.set_obligation_evar sigma (fst (destEvar sigma evc))
+  | _ -> sigma
 
 (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [sigma] and *)
 (* the type constraint tycon *)
 
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
-  let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in
+let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+  let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
   let pretype_type = pretype_type k0 resolve_tc in
   let pretype = pretype k0 resolve_tc in
   let open Context.Rel.Declaration in
@@ -477,7 +477,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon
 
   | GVar id ->
-    let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in
+    let sigma, t_id = pretype_id (fun e r t -> pretype ~program_mode tycon e r t) k0 loc env sigma id in
     inh_conv_coerce_to_tycon ?loc env sigma t_id tycon
 
   | GEvar (id, inst) ->
@@ -488,7 +488,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         try Evd.evar_key id sigma
         with Not_found -> error_evar_not_found ?loc !!env sigma id in
       let hyps = evar_filtered_context (Evd.find sigma evk) in
-      let sigma, args = pretype_instance k0 resolve_tc env sigma loc hyps evk inst in
+      let sigma, args = pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = Retyping.get_judgment_of !!env sigma c in
       inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -513,7 +513,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         | Some ty -> sigma, ty
         | None -> new_type_evar env sigma loc in
       let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
-      let sigma = mark_obligation_evar sigma k uj_val in
+      let sigma = if program_mode then mark_obligation_evar sigma k uj_val else sigma in
       sigma, { uj_val; uj_type = ty }
 
   | GHole (k, _naming, Some arg) ->
@@ -525,24 +525,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       sigma, { uj_val = c; uj_type = ty }
 
   | GRec (fixkind,names,bl,lar,vdef) ->
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let rec type_bl env sigma ctxt = function
       | [] -> sigma, ctxt
       | (na,bk,None,ty)::bl ->
-        let sigma, ty' = pretype_type empty_valcon env sigma ty in
-	let dcl = LocalAssum (na, ty'.utj_val) in
-        let dcl', env = push_rel sigma dcl env in
+        let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in
+        let dcl = LocalAssum (na, ty'.utj_val) in
+        let dcl', env = push_rel ~hypnaming sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
-        let sigma, ty' = pretype_type empty_valcon env sigma ty in
-        let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in
+        let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in
+        let sigma, bd' = pretype ~program_mode (mk_tycon ty'.utj_val) env sigma bd in
         let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
-        let dcl', env = push_rel sigma dcl env in
+        let dcl', env = push_rel ~hypnaming sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl in
     let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in
     let sigma, larj =
       Array.fold_left2_map
         (fun sigma e ar ->
-          pretype_type empty_valcon (snd (push_rel_context sigma e env)) sigma ar)
+          pretype_type ~program_mode empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar)
         sigma ctxtv lar in
     let lara = Array.map (fun a -> a.utj_val) larj in
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -562,7 +563,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       | None -> sigma
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-    let names,newenv = push_rec_types sigma (names,ftys) env in
+    let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in
     let sigma, vdefj =
       Array.fold_left2_map_i
         (fun i sigma ctxt def ->
@@ -571,8 +572,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
            let (ctxt,ty) =
              decompose_prod_n_assum sigma (Context.Rel.length ctxt)
                (lift nbfix ftys.(i)) in
-           let ctxt,nenv = push_rel_context sigma ctxt newenv in
-           let sigma, j = pretype (mk_tycon ty) nenv sigma def in
+           let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in
+           let sigma, j = pretype ~program_mode (mk_tycon ty) nenv sigma def in
            sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
                     uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         sigma ctxtv vdef in
@@ -618,14 +619,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     inh_conv_coerce_to_tycon ?loc env sigma j tycon
 
   | GApp (f,args) ->
-    let sigma, fj = pretype empty_tycon env sigma f in
+    let sigma, fj = pretype ~program_mode empty_tycon env sigma f in
     let floc = loc_of_glob_constr f in
     let length = List.length args in
     let candargs =
 	(* Bidirectional typechecking hint: 
 	   parameters of a constructor are completely determined
 	   by a typing constraint *)
-      if Flags.is_program_mode () && length > 0 && isConstruct sigma fj.uj_val then
+      if program_mode && length > 0 && isConstruct sigma fj.uj_val then
 	match tycon with
 	| None -> []
 	| Some ty ->
@@ -656,12 +657,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       | [] -> sigma, resj
       | c::rest ->
         let argloc = loc_of_glob_constr c in
-        let sigma, resj = Coercion.inh_app_fun resolve_tc !!env sigma resj in
+        let sigma, resj = Coercion.inh_app_fun ~program_mode resolve_tc !!env sigma resj in
         let resty = whd_all !!env sigma resj.uj_type in
         match EConstr.kind sigma resty with
         | Prod (na,c1,c2) ->
           let tycon = Some c1 in
-          let sigma, hj = pretype tycon env sigma c in
+          let sigma, hj = pretype ~program_mode tycon env sigma c in
           let sigma, candargs, ujval =
             match candargs with
             | [] -> sigma, [], j_val hj
@@ -678,7 +679,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	    let j = { uj_val = value; uj_type = typ } in
             apply_rec env sigma (n+1) j candargs rest
 	  | _ ->
-            let sigma, hj = pretype empty_tycon env sigma c in
+            let sigma, hj = pretype ~program_mode empty_tycon env sigma c in
 	      error_cant_apply_not_functional
                 ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|]
     in
@@ -703,29 +704,31 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       match tycon with
       | None -> sigma, tycon
       | Some ty ->
-        let sigma, ty' = Coercion.inh_coerce_to_prod ?loc !!env sigma ty in
+        let sigma, ty' = Coercion.inh_coerce_to_prod ?loc ~program_mode !!env sigma ty in
         sigma, Some ty'
     in
     let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in
     let dom_valcon = valcon_of_tycon dom in
-    let sigma, j = pretype_type dom_valcon env sigma c1 in
+    let sigma, j = pretype_type ~program_mode dom_valcon env sigma c1 in
     let var = LocalAssum (name, j.utj_val) in
-    let var',env' = push_rel sigma var env in
-    let sigma, j' = pretype rng env' sigma c2 in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let var',env' = push_rel ~hypnaming sigma var env in
+    let sigma, j' = pretype ~program_mode rng env' sigma c2 in
     let name = get_name var' in
     let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
     inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
   | GProd(name,bk,c1,c2) ->
-    let sigma, j = pretype_type empty_valcon env sigma c1 in
+    let sigma, j = pretype_type ~program_mode empty_valcon env sigma c1 in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let sigma, name, j' = match name with
       | Anonymous ->
-        let sigma, j = pretype_type empty_valcon env sigma c2 in
+        let sigma, j = pretype_type ~program_mode empty_valcon env sigma c2 in
         sigma, name, { j with utj_val = lift 1 j.utj_val }
       | Name _ ->
         let var = LocalAssum (name, j.utj_val) in
-        let var, env' = push_rel sigma var env in
-        let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in
+        let var, env' = push_rel ~hypnaming sigma var env in
+        let sigma, c2_j = pretype_type ~program_mode empty_valcon env' sigma c2 in
         sigma, get_name var, c2_j
     in
     let resj =
@@ -741,23 +744,24 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
     let sigma, tycon1 =
       match t with
       | Some t ->
-        let sigma, t_j = pretype_type empty_valcon env sigma t in
+        let sigma, t_j = pretype_type ~program_mode empty_valcon env sigma t in
         sigma, mk_tycon t_j.utj_val
       | None ->
         sigma, empty_tycon in
-    let sigma, j = pretype tycon1 env sigma c1 in
+    let sigma, j = pretype ~program_mode tycon1 env sigma c1 in
     let sigma, t = Evarsolve.refresh_universes
       ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma j.uj_type in
     let var = LocalDef (name, j.uj_val, t) in
     let tycon = lift_tycon 1 tycon in
-    let var, env = push_rel sigma var env in
-    let sigma, j' = pretype tycon env sigma c2 in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let var, env = push_rel ~hypnaming sigma var env in
+    let sigma, j' = pretype ~program_mode tycon env sigma c2 in
     let name = get_name var in
     sigma, { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
              uj_type = subst1 j.uj_val j'.uj_type }
 
   | GLetTuple (nal,(na,po),c,d) ->
-    let sigma, cj = pretype empty_tycon env sigma c in
+    let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
     let (IndType (indf,realargs)) =
       try find_rectype !!env sigma cj.uj_type
       with Not_found ->
@@ -792,7 +796,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	  | _ -> assert false
 	in aux 1 1 (List.rev nal) cs.cs_args, true in
     let fsign = Context.Rel.map (whd_betaiota sigma) fsign in
-    let fsign,env_f = push_rel_context sigma fsign env in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+    let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
     let obj ind p v f =
       if not record then
 	let f = it_mkLambda_or_LetIn f fsign in
@@ -810,10 +815,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
       let nar = List.length arsgn in
-      let psign',env_p = push_rel_context ~force_names:true sigma psign predenv in
+      let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in
 	  (match po with
 	  | Some p ->
-            let sigma, pj = pretype_type empty_valcon env_p sigma p in
+            let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in
             let ccl = nf_evar sigma pj.utj_val in
 	    let p = it_mkLambda_or_LetIn ccl psign' in
 	    let inst =
@@ -821,7 +826,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	      @[EConstr.of_constr (build_dependent_constructor cs)] in
 	    let lp = lift cs.cs_nargs p in
             let fty = hnf_lam_applist !!env sigma lp inst in
-            let sigma, fj = pretype (mk_tycon fty) env_f sigma d in
+            let sigma, fj = pretype ~program_mode (mk_tycon fty) env_f sigma d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
                 Typing.check_allowed_sort !!env sigma ind cj.uj_val p;
@@ -831,7 +836,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 
 	  | None ->
 	    let tycon = lift_tycon cs.cs_nargs tycon in
-            let sigma, fj = pretype tycon env_f sigma d in
+            let sigma, fj = pretype ~program_mode tycon env_f sigma d in
             let ccl = nf_evar sigma fj.uj_type in
 	    let ccl =
               if noccur_between sigma 1 cs.cs_nargs ccl then
@@ -848,7 +853,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
             in sigma, { uj_val = v; uj_type = ccl })
 
   | GIf (c,(na,po),b1,b2) ->
-    let sigma, cj = pretype empty_tycon env sigma c in
+    let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
     let (IndType (indf,realargs)) =
       try find_rectype !!env sigma cj.uj_type
       with Not_found ->
@@ -869,10 +874,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
       let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
       let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
-      let psign,env_p = push_rel_context sigma psign predenv in
+    let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
+      let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in
       let sigma, pred, p = match po with
 	| Some p ->
-          let sigma, pj = pretype_type empty_valcon env_p sigma p in
+          let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in
           let ccl = nf_evar sigma pj.utj_val in
           let pred = it_mkLambda_or_LetIn ccl psign in
           let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in
@@ -894,8 +900,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	let csgn =
           List.map (set_name Anonymous) cs_args
         in
-        let _,env_c = push_rel_context sigma csgn env in
-        let sigma, bj = pretype (mk_tycon pi) env_c sigma b in
+        let _,env_c = push_rel_context ~hypnaming sigma csgn env in
+        let sigma, bj = pretype ~program_mode (mk_tycon pi) env_c sigma b in
         sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in
       let sigma, b1 = f sigma cstrs.(0) b1 in
       let sigma, b2 = f sigma cstrs.(1) b2 in
@@ -910,23 +916,23 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
       inh_conv_coerce_to_tycon ?loc env sigma cj tycon
 
   | GCases (sty,po,tml,eqns) ->
-    Cases.compile_cases ?loc sty (pretype, sigma) tycon env (po,tml,eqns)
+    Cases.compile_cases ?loc ~program_mode sty (pretype ~program_mode, sigma) tycon env (po,tml,eqns)
 
   | GCast (c,k) ->
     let sigma, cj =
       match k with
       | CastCoerce ->
-        let sigma, cj = pretype empty_tycon env sigma c in
-        Coercion.inh_coerce_to_base ?loc !!env sigma cj
+        let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
+        Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj
       | CastConv t | CastVM t | CastNative t ->
         let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
-        let sigma, tj = pretype_type empty_valcon env sigma t in
+        let sigma, tj = pretype_type ~program_mode empty_valcon env sigma t in
         let sigma, tval = Evarsolve.refresh_universes
             ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in
         let tval = nf_evar sigma tval in
         let (sigma, cj), tval = match k with
 	  | VMcast ->
-            let sigma, cj = pretype empty_tycon env sigma c in
+            let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
             let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in
               if not (occur_existential sigma cty || occur_existential sigma tval) then
                 match Reductionops.vm_infer_conv !!env sigma cty tval with
@@ -937,7 +943,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
 	      else user_err ?loc  (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
-            let sigma, cj = pretype empty_tycon env sigma c in
+            let sigma, cj = pretype ~program_mode empty_tycon env sigma c in
             let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in
             begin
               match Nativenorm.native_infer_conv !!env sigma cty tval with
@@ -947,7 +953,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
                   (ConversionFailed (!!env,cty,tval))
             end
           | _ ->
-            pretype (mk_tycon tval) env sigma c, tval
+            pretype ~program_mode (mk_tycon tval) env sigma c, tval
         in
         let v = mkCast (cj.uj_val, k, tval) in
         sigma, { uj_val = v; uj_type = tval }
@@ -961,7 +967,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         in
         inh_conv_coerce_to_tycon ?loc env sigma resj tycon
 
-and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
   let f decl (subst,update,sigma) =
     let id = NamedDecl.get_id decl in
     let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -993,7 +999,7 @@ and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
     let sigma, c, update =
       try
         let c = List.assoc id update in
-        let sigma, c = pretype k0 resolve_tc (mk_tycon t) env sigma c in
+        let sigma, c = pretype ~program_mode k0 resolve_tc (mk_tycon t) env sigma c in
         check_body sigma id (Some c.uj_val);
         sigma, c.uj_val, List.remove_assoc id update
       with Not_found ->
@@ -1018,7 +1024,7 @@ and pretype_instance k0 resolve_tc env sigma loc hyps evk update =
   sigma, Array.map_of_list snd subst
 
 (* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
   | GHole (knd, naming, None) ->
       let loc = loc_of_glob_constr c in
       (match valcon with
@@ -1042,10 +1048,10 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
        | None ->
          let sigma, s = new_sort_variable univ_flexible_alg sigma in
          let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in
-         let sigma = mark_obligation_evar sigma knd utj_val in
+         let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
          sigma, { utj_val; utj_type = s})
   | _ ->
-      let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode k0 resolve_tc empty_tycon env sigma c in
       let loc = loc_of_glob_constr c in
       let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
 	match valcon with
@@ -1059,17 +1065,21 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get
           end
 
 let ise_pretype_gen flags env sigma lvar kind c =
-  let env = GlobEnv.make env sigma lvar in
+  let program_mode = flags.program_mode in
+  let hypnaming =
+    if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
+  in
+  let env = GlobEnv.make ~hypnaming env sigma lvar in
   let k0 = Context.Rel.length (rel_context !!env) in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint ->
-      let sigma, j = pretype k0 flags.use_typeclasses empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode k0 flags.use_typeclasses empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
-      let sigma, j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+      let sigma, j = pretype ~program_mode k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
       sigma, j.uj_val, j.uj_type
     | IsType ->
-      let sigma, tj = pretype_type k0 flags.use_typeclasses empty_valcon env sigma c in
+      let sigma, tj = pretype_type ~program_mode k0 flags.use_typeclasses empty_valcon env sigma c in
       sigma, tj.utj_val, mkSort tj.utj_type
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)
@@ -1078,13 +1088,17 @@ let default_inference_flags fail = {
   use_typeclasses = true;
   solve_unification_constraints = true;
   fail_evar = fail;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let no_classes_no_fail_inference_flags = {
   use_typeclasses = false;
   solve_unification_constraints = true;
   fail_evar = false;
-  expand_evars = true }
+  expand_evars = true;
+  program_mode = false;
+}
 
 let all_and_fail_flags = default_inference_flags true
 let all_no_fail_flags = default_inference_flags false
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 59e6c00037a7..3c875e69d206 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -36,7 +36,8 @@ type inference_flags = {
   use_typeclasses : bool;
   solve_unification_constraints : bool;
   fail_evar : bool;
-  expand_evars : bool
+  expand_evars : bool;
+  program_mode : bool;
 }
 
 val default_inference_flags : bool -> inference_flags
@@ -101,7 +102,7 @@ val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
     reporting an appropriate error message *)
 
 val check_evars_are_solved :
-  env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
+  program_mode:bool -> env -> ?initial:evar_map -> (* current map: *) evar_map -> unit
 
 (** [check_evars env initial_sigma extended_sigma c] fails if some
    new unresolved evar remains in [c] *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e4d96da0a68b..ac0b58b92bb1 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1269,7 +1269,7 @@ let is_mimick_head sigma ts f =
 
 let try_to_coerce env evd c cty tycon =
   let j = make_judge c cty in
-  let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in
+  let (evd',j') = inh_conv_coerce_rigid_to ~program_mode:false true env evd j tycon in
   let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
   let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
     (evd',j'.uj_val)
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 1f1bdf4da794..9540d3de44d8 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -677,7 +677,7 @@ let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma ev in
   let ty = Retyping.get_type_of env sigma c in
   let j = Environ.make_judge c ty in
-  let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
+  let (sigma, j) = Coercion.inh_conv_coerce_to ~program_mode:false true env sigma j t in
   let (ev, _) = destEvar sigma ev in
   let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6c4193c66b94..1b2756f49f42 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -53,7 +53,9 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.use_typeclasses = true;
       Pretyping.solve_unification_constraints = true;
       Pretyping.fail_evar = false;
-      Pretyping.expand_evars = true } in
+      Pretyping.expand_evars = true;
+      Pretyping.program_mode = false;
+    } in
     try Pretyping.understand_ltac flags
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1d796fece504..06e6b89df1ab 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -137,26 +137,6 @@ let refine ~typecheck f =
   in
   Proofview.Goal.enter (make_refine_enter ~typecheck f)
 
-(** Useful definitions *)
-
-let with_type env evd c t =
-  let my_type = Retyping.get_type_of env evd c in
-  let j = Environ.make_judge c my_type in
-  let (evd,j') =
-    Coercion.inh_conv_coerce_to true env evd j t
-  in
-  evd , j'.Environ.uj_val
-
-let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
-  let concl = Proofview.Goal.concl gl in
-  let env = Proofview.Goal.env gl in
-  let f h =
-    let (h, c) = f h in
-    with_type env h c concl
-  in
-  refine ~typecheck f
-end
-
 (** {7 solve_constraints}
 
   Ensure no remaining unification problems are left. Run at every "." by default. *)
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 1af6463a0297..55dafe521f7f 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -34,17 +34,6 @@ val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
 
-(** {7 Helper functions} *)
-
-val with_type : Environ.env -> Evd.evar_map ->
-  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
-(** [with_type env sigma c t] ensures that [c] is of type [t]
-    inserting a coercion if needed. *)
-
-val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
-(** Like {!refine} except the refined term is coerced to the conclusion of the
-    current goal. *)
-
 (** {7 Unification constraint handling} *)
 
 val solve_constraints : unit tactic
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 42540af99136..feb8e2a67fe8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -56,6 +56,7 @@ let options_affecting_stm_scheduling =
   [ Attributes.universe_polymorphism_option_name;
     stm_allow_nested_proofs_option_name;
     Vernacentries.proof_mode_opt_name;
+    Attributes.program_mode_option_name;
   ]
 
 let classify_vernac e =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 356b43ec1407..48997163de1c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -250,7 +250,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
 let add_inversion_lemma_exn ~poly na com comsort bool tac =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let sigma, c = Constrintern.interp_type_evars env sigma com in
+  let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
   let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
   try
     add_inversion_lemma ~poly na env sigma c sort bool tac
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 070b2356e5e0..afa623741af0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1155,7 +1155,9 @@ let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
   Pretyping.fail_evar = not with_evar;
-  Pretyping.expand_evars = true }
+  Pretyping.expand_evars = true;
+  Pretyping.program_mode = false;
+}
 
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index b80e0bb0e47b..e28314cada33 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -82,7 +82,7 @@ Notation "F ^op" := (OppositeFunctor F) : functor_scope.
 Definition FunctorProduct' C D C' D' (F : Functor C D) (F' : Functor C' D') : Functor (C * C') (D * D')
   := admit.
 
-Global Class FunctorApplicationInterpretable
+Class FunctorApplicationInterpretable
        {C D} (F : Functor C D)
        {argsT : Type} (args : argsT)
        {T : Type} (rtn : T)
diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
index 19551dc92e87..72bc04e05e4a 100644
--- a/test-suite/bugs/closed/HoTT_coq_061.v
+++ b/test-suite/bugs/closed/HoTT_coq_061.v
@@ -96,7 +96,7 @@ Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F'
   := Build_NaturalTransformation (F o G) (F' o G)
                                  (fun c => T (G c))
                                  admit.
-Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
+Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
 
 Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
 Notation "T 'o' U"
diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
index a80d075f6937..cd6539b51ccf 100644
--- a/test-suite/bugs/closed/HoTT_coq_120.v
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -89,7 +89,7 @@ Definition set_cat : PreCategory
   := @Build_PreCategory hSet
                         (fun x y => forall _ : x, y)%core
                         (fun _ _ _ f g x => f (g x))%core.
-Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
+Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
 Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
 Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
 Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
diff --git a/test-suite/bugs/closed/bug_3427.v b/test-suite/bugs/closed/bug_3427.v
index 317efb0b3211..f00d2fcf0962 100644
--- a/test-suite/bugs/closed/bug_3427.v
+++ b/test-suite/bugs/closed/bug_3427.v
@@ -146,7 +146,7 @@ Section Univalence.
     := (equiv_path A B)^-1 f.
 End Univalence.
 
-Local Inductive minus1Trunc (A :Type) : Type :=
+Inductive minus1Trunc (A :Type) : Type :=
   min1 : A -> minus1Trunc A.
 
 Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0.
diff --git a/test-suite/bugs/closed/bug_7795.v b/test-suite/bugs/closed/bug_7795.v
index 5db0f81cc512..5f9d42f5f7e2 100644
--- a/test-suite/bugs/closed/bug_7795.v
+++ b/test-suite/bugs/closed/bug_7795.v
@@ -52,6 +52,8 @@ Definition hh:
          false = true.
 Admitted.
 
+Require Import Program.
+
 Set Program Mode. (* removing this line prevents the bug *)
 Obligation Tactic := repeat t_base.
 
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 4f238f38e6f1..9b8c4efb3765 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -125,11 +125,25 @@ let qualify_attribute qual (parser:'a attribute) : 'a attribute =
     let extra = if rem = [] then extra else (qual, VernacFlagList rem) :: extra in
     extra, v
 
+(** [program_mode] tells that Program mode has been activated, either
+    globally via [Set Program] or locally via the Program command prefix. *)
+
+let program_mode_option_name = ["Program";"Mode"]
+let program_mode = ref false
+
+let () = let open Goptions in
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "use of the program extension";
+      optkey   = program_mode_option_name;
+      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 (Flags.is_program_mode())
+  | None -> return (!program_mode)
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 66e10f94cd81..3cb4d69ca072 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -53,7 +53,7 @@ val template : bool option attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
 
-val program_opt : bool option attribute
+val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
 
 val only_locality : vernac_flags -> bool option
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dd49f09d3538..ea434dbc4f64 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -82,14 +82,14 @@ let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
-let type_ctx_instance env sigma ctx inst subst =
+let type_ctx_instance ~program_mode env sigma ctx inst subst =
   let open Vars in
   let rec aux (sigma, subst, instctx) l = function
     decl :: ctx ->
       let t' = substl subst (RelDecl.get_type decl) in
       let (sigma, c'), l =
 	match decl with
-        | LocalAssum _ -> interp_casted_constr_evars env sigma (List.hd l) t', List.tl l
+        | LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l
         | LocalDef (_,b,_) -> (sigma, substl subst b), l
       in
       let d = RelDecl.get_name decl, Some c', t' in
@@ -206,7 +206,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
     | None ->
       (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma
     | Some (Inr term) ->
-      let sigma, c = interp_casted_constr_evars env' sigma term cty in
+      let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in
       Some (Inr (c, subst)), sigma
     | Some (Inl props) ->
       let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in
@@ -237,7 +237,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
         unbound_method env' k.cl_impl (get_id n)
       | _ ->
         let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in
-        let sigma, res = type_ctx_instance (push_rel_context ctx' env') sigma kcl_props props subst in
+        let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in
         Some (Inl res), sigma
   in
   let term, termtype =
@@ -276,7 +276,7 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
   else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
   id
 
-let interp_instance_context env ctx ?(generalize=false) pl bk cl =
+let interp_instance_context ~program_mode 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
@@ -295,8 +295,8 @@ let interp_instance_context env ctx ?(generalize=false) pl bk cl =
     if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass)
     else tclass
   in
-  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 sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
+  let sigma, (c', imps') = interp_type_evars_impls ~program_mode ~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
@@ -324,7 +324,7 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
   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
+    interp_instance_context ~program_mode env ~generalize ctx pl bk cl
   in
   let id =
     match instid with
@@ -337,11 +337,11 @@ let new_instance ?(global=false) ?(refine= !refine_instance) ~program_mode
   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 declare_new_instance ?(global=false) ~program_mode 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
+    interp_instance_context ~program_mode env ctx pl bk cl
   in
   do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
 
@@ -361,7 +361,7 @@ let named_of_rel_context 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 env sigma l in
+  let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
   (* Note, we must use the normalized evar from now on! *)
   let sigma = Evd.minimize_universes sigma in
   let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 6f61da66cf99..7e0ec4262528 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -55,6 +55,7 @@ val new_instance :
 
 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 ->
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 7301e1fff7d8..73d0be04df35 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -84,8 +84,8 @@ match local with
   in
     (gr,inst,Lib.is_modtype_strict ())
 
-let interp_assumption sigma env impls c =
-  let sigma, (ty, impls) = interp_type_evars_impls env sigma ~impls c in
+let interp_assumption ~program_mode sigma env impls c =
+  let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
   sigma, (ty, impls)
 
 (* When monomorphic the universe constraints are declared with the first declaration only. *)
@@ -131,7 +131,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 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
@@ -147,7 +147,7 @@ let do_assumptions kind nl l =
   in
   (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
-    let sigma,(t,imps) = interp_assumption sigma env ienv c in
+    let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
     let env =
       EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index c5bf3725a9b2..385ec33beaa2 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,7 +17,7 @@ open Decl_kinds
 
 (** {6 Parameters/Assumptions} *)
 
-val do_assumptions : locality * polymorphic * assumption_object_kind ->
+val do_assumptions : program_mode:bool -> locality * polymorphic * assumption_object_kind ->
   Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool
 
 (************************************************************************)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 79d45880fc58..5e74114a86c9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -41,26 +41,26 @@ let check_imps ~impsty ~impsbody =
   in
   if not b then warn_implicits_in_term ()
 
-let interp_definition pl bl poly red_option c ctypopt =
+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
   (* Build the parameters *)
-  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
+  let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in
   (* Build the type *)
   let evd, tyopt = Option.fold_left_map
-      (interp_type_evars_impls ~impls env_bl)
+      (interp_type_evars_impls ~program_mode ~impls env_bl)
       evd ctypopt
   in
   (* Build the body, and merge implicits from parameters and from type/body *)
   let evd, c, imps, tyopt =
     match tyopt with
     | None ->
-      let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in
+      let evd, (c, impsbody) = interp_constr_evars_impls ~program_mode ~impls env_bl evd c in
       evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None
     | Some (ty, impsty) ->
-      let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in
+      let evd, (c, impsbody) = interp_casted_constr_evars_impls ~program_mode ~impls env_bl evd c ty in
       check_imps ~impsty ~impsbody;
       evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty
   in
@@ -85,14 +85,14 @@ let interp_definition pl bl poly red_option c ctypopt =
   let ce = definition_entry ?types:tyopt ~univs:uctx c in
   (ce, evd, decl, imps)
 
-let check_definition (ce, evd, _, imps) =
+let check_definition ~program_mode (ce, evd, _, imps) =
   let env = Global.env () in
-  check_evars_are_solved env evd;
+  check_evars_are_solved ~program_mode env evd;
   ce
 
 let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
-    interp_definition univdecl bl (pi2 k) red_option c ctypopt
+    interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
   in
     if program_mode then
       let env = Global.env () in
@@ -111,5 +111,5 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
       let univ_hook = Obligations.mk_univ_hook (fun _ _ l r -> Lemmas.call_hook ?hook l r) in
       ignore(Obligations.add_definition
           ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~univ_hook obls)
-    else let ce = check_definition def in
+    else let ce = check_definition ~program_mode def in
       ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps ?hook)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 0ac5762f7197..9cb6190fcc89 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -27,7 +27,7 @@ val do_definition : program_mode:bool ->
 (************************************************************************)
 
 (** Not used anywhere. *)
-val interp_definition :
+val interp_definition : program_mode:bool ->
   universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
                         UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 77227b64e6c0..5229d9e8e835 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -116,21 +116,23 @@ type structured_fixpoint_expr = {
   fix_type : constr_expr
 }
 
-let interp_fix_context ~cofix env sigma fix =
+let interp_fix_context ~program_mode ~cofix env sigma fix =
   let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
-  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars env sigma before in
-  let sigma, (impl_env', ((env'', ctx'), imps')) = interp_context_evars ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after in
+  let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
+  let sigma, (impl_env', ((env'', ctx'), imps')) =
+    interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
+  in
   let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
-let interp_fix_ccl sigma impls (env,_) fix =
-  interp_type_evars_impls ~impls env sigma fix.fix_type
+let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
+  interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type
 
-let interp_fix_body env_rec sigma impls (_,ctx) fix ccl =
+let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
   let open EConstr in
   Option.cata (fun body ->
     let env = push_rel_context ctx env_rec in
-    let sigma, body = interp_casted_constr_evars env sigma ~impls body ccl in
+    let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in
     sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body
 
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
@@ -184,11 +186,11 @@ let interp_recursive ~program_mode ~cofix fixl notations =
   let sigma, decl = interp_univ_decl_opt env all_universes in
   let sigma, (fixctxs, fiximppairs, fixannots) =
     on_snd List.split3 @@
-      List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in
+      List.fold_left_map (fun sigma -> interp_fix_context ~program_mode env sigma ~cofix) sigma fixl in
   let fixctximpenvs, fixctximps = List.split fiximppairs in
   let sigma, (fixccls,fixcclimps) =
     on_snd List.split @@
-      List.fold_left3_map interp_fix_ccl sigma fixctximpenvs fixctxs fixl in
+      List.fold_left3_map (interp_fix_ccl ~program_mode) sigma fixctximpenvs fixctxs fixl in
   let fixtypes = List.map2 build_fix_type fixctxs fixccls in
   let fixtypes = List.map (fun c -> nf_evar sigma c) fixtypes in
   let fiximps = List.map3
@@ -220,7 +222,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
     Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
       List.fold_left4_map
-        (fun sigma fixctximpenv -> interp_fix_body env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
+        (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
         sigma fixctximpenvs fixctxs fixl fixccls)
       () in
 
@@ -239,7 +241,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) =
   end
 
 let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) =
-  check_evars_are_solved env evd;
+  check_evars_are_solved ~program_mode:false env evd;
   let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in
   let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
   Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index afee2a58687b..68ad276113f7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -162,7 +162,7 @@ let interp_cstrs env sigma impls mldata arity ind =
   let sigma, (ctyps'', cimpls) =
     on_snd List.split @@
     List.fold_left_map (fun sigma l ->
-        interp_type_evars_impls env sigma ~impls l) sigma ctyps' in
+        interp_type_evars_impls ~program_mode:false env sigma ~impls l) sigma ctyps' in
   sigma, (cnames, ctyps'', cimpls)
 
 let sign_level env evd sign =
@@ -358,9 +358,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   then user_err (str "Inductives with uniform parameters may not have attached notations.");
   let sigma, udecl = interp_univ_decl_opt env0 udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
-    interp_context_evars env0 sigma uparamsl in
+    interp_context_evars ~program_mode:false env0 sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
-    interp_context_evars ~impl_env:uimpls env_uparams sigma paramsl
+    interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
   in
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index edce8e255cb9..a30313d37c07 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -91,17 +91,17 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
-  let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in
+  let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars ~program_mode:true env sigma bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
-  let sigma, top_arity = interp_type_evars top_env sigma arityc in
+  let sigma, top_arity = interp_type_evars ~program_mode:true top_env sigma arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
   let argname = Id.of_string "recarg" in
   let arg = LocalAssum (Name argname, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
-  let sigma, (rel, _) = interp_constr_evars_impls env sigma r in
+  let sigma, (rel, _) = interp_constr_evars_impls ~program_mode:true env sigma r in
   let relty = Typing.unsafe_type_of env sigma rel in
   let relargty =
     let error () =
@@ -117,7 +117,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
           | _, _ -> error ()
       with e when CErrors.noncritical e -> error ()
   in
-  let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in
+  let sigma, measure = interp_casted_constr_evars ~program_mode:true binders_env sigma measure relargty in
   let sigma, wf_rel, wf_rel_fun, measure_fn =
     let measure_body, measure =
       it_mkLambda_or_LetIn measure letbinders,
@@ -176,7 +176,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     let newimpls = Id.Map.singleton recname
         (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
          scopes @ [None]) in
-    interp_casted_constr_evars (push_rel_context ctx env) sigma
+    interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
       ~impls:newimpls body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 41057f8ab249..361ed1a73725 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -57,7 +57,7 @@ let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
-  if not allow_evars then Pretyping.check_evars_are_solved env sigma
+  if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
 
 let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body =
   check_definition_evars ~allow_evars sigma;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 0dfbba0e835b..4635883dc288 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -417,14 +417,14 @@ let start_proof_with_initialization ?hook kind sigma decl recguard thms snl =
           | None -> p,(true,[])
           | Some tac -> Proof.run_tactic Global.(env ()) tac p))
 
-let start_proof_com ?inference_hook ?hook kind thms =
+let start_proof_com ~program_mode ?inference_hook ?hook kind thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
   let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
-    let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
-    let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
-    let flags = all_and_fail_flags in
+    let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in
+    let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in
+    let flags = { all_and_fail_flags with program_mode } in
     let hook = inference_hook in
     let evd = solve_remaining_evars ?hook flags env evd in
     let ids = List.map RelDecl.get_name ctx in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 3ac12d3b0bc9..a9a10a6e381a 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -31,7 +31,7 @@ val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.eva
   ?univ_hook:(UState.t option -> declaration_hook) -> EConstr.types -> unit
 
 val start_proof_com :
-  ?inference_hook:Pretyping.inference_hook ->
+  program_mode:bool -> ?inference_hook:Pretyping.inference_hook ->
   ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list ->
   unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6642d04c9874..601445210772 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1197,15 +1197,7 @@ let next_obligation n tac =
   in
   solve_obligation prg i tac
 
-let init_program () =
+let check_program_libraries () =
   Coqlib.check_required_library Coqlib.datatypes_module_name;
   Coqlib.check_required_library ["Coq";"Init";"Specif"];
   Coqlib.check_required_library ["Coq";"Program";"Tactics"]
-
-let set_program_mode c =
-  if c then
-    if !Flags.program_mode then ()
-    else begin
-      init_program ();
-      Flags.program_mode := true;
-    end
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index c670e3a3b533..4eef668f5627 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -110,7 +110,7 @@ exception NoObligations of Names.Id.t option
 
 val explain_no_obligations : Names.Id.t option -> Pp.t
 
-val set_program_mode : bool -> unit
+val check_program_libraries : unit -> unit
 
 type program_info
 val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag
diff --git a/vernac/record.ml b/vernac/record.ml
index 1b7b828f477f..247e0790d799 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -65,10 +65,10 @@ let () =
 let interp_fields_evars env sigma impls_env nots l =
   List.fold_left2
     (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) ->
-      let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in
+      let sigma, (t', impl) = interp_type_evars_impls ~program_mode:false env sigma ~impls t in
       let sigma, b' =
         Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@
-                      interp_casted_constr_evars_impls env sigma ~impls x t') (sigma,None) b in
+                      interp_casted_constr_evars_impls ~program_mode:false env sigma ~impls x t') (sigma,None) b in
       let impls =
 	match i with
 	| Anonymous -> impls
@@ -116,14 +116,14 @@ let typecheck_params_and_fields finite def poly pl ps records =
            | CLocalPattern {CAst.loc} ->
               Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
   in 
-  let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in
+  let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in
   let fold (sigma, template) (_, t, _, _) = match t with
     | Some t -> 
        let env = EConstr.push_rel_context newps env0 in
        let poly =
          match t with
          | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in
-       let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in
+       let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_allnolet env sigma s in
          (match EConstr.kind sigma sred with
 	 | Sort s' ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 76113551009a..eb263757e2ee 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -514,9 +514,9 @@ let () =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print ?hook k l =
+let start_proof_and_print ~program_mode ?hook k l =
   let inference_hook =
-    if Flags.is_program_mode () then
+    if program_mode then
       let hook env sigma ev =
         let tac = !Obligations.default_tactic in
         let evi = Evd.find sigma ev in
@@ -536,7 +536,7 @@ let start_proof_and_print ?hook k l =
       in Some hook
     else None
   in
-  start_proof_com ?inference_hook ?hook k l
+  start_proof_com ~program_mode ?inference_hook ?hook k l
 
 let vernac_definition_hook p = function
 | Coercion ->
@@ -549,7 +549,6 @@ let vernac_definition_hook p = function
 
 let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
   let open DefAttributes in
-  let atts = parse atts in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let () =
@@ -560,7 +559,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
       | Discharge -> Dumpglob.dump_definition lid true "var"
       | Local | Global -> Dumpglob.dump_definition lid false "def"
   in
-  let program_mode = Flags.is_program_mode () in
+  let program_mode = atts.program in
   let name =
     match id with
     | Anonymous -> fresh_name_for_anonymous_theorem ()
@@ -568,7 +567,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
-      start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
+      start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind)
         ?hook [(CAst.make ?loc name, pl), (bl, t)]
     | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
@@ -581,11 +580,10 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
 
 let vernac_start_proof ~atts kind l =
   let open DefAttributes in
-  let atts = parse atts in
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_proof_and_print (local, atts.polymorphic, Proof kind) l
+  start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l
 
 let vernac_end_proof ?proof = function
   | Admitted          -> save_proof ?proof Admitted
@@ -600,7 +598,6 @@ let vernac_exact_proof c =
 
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
-  let atts = parse atts in
   let local = enforce_locality_exp atts.locality discharge in
   let global = local == Global in
   let kind = local, atts.polymorphic, kind in
@@ -609,7 +606,7 @@ let vernac_assumption ~atts 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 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 should_treat_as_cumulative cum poly =
@@ -675,9 +672,7 @@ let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive ~atts cum lo finite indl =
-  let open DefAttributes in
-  let atts, template = Attributes.(parse_with_extra template atts) in
-  let atts = parse atts in
+  let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -708,7 +703,7 @@ let vernac_inductive ~atts cum lo finite indl =
     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
-    vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+    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 *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -731,7 +726,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let ((_, _, _, kind, _), _) = List.hd indl in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record ~template udecl cum kind atts.polymorphic finite recordl
+    vernac_record ~template udecl cum kind poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
     let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -755,9 +750,9 @@ let vernac_inductive ~atts cum lo finite indl =
     | RecordDecl _ -> assert false (* ruled out above *)
     in
     let indl = List.map unpack indl in
-    let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
+    let is_cumulative = should_treat_as_cumulative cum poly in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative poly lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 (*
@@ -773,12 +768,11 @@ let vernac_inductive ~atts cum lo finite indl =
 
 let vernac_fixpoint ~atts discharge l =
   let open DefAttributes in
-  let atts = parse atts in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   (* XXX: Switch to the attribute system and match on ~atts *)
-  let do_fixpoint = if Flags.is_program_mode () then
+  let do_fixpoint = if atts.program then
       ComProgramFixpoint.do_fixpoint
     else
       ComFixpoint.do_fixpoint
@@ -787,11 +781,10 @@ let vernac_fixpoint ~atts discharge l =
 
 let vernac_cofixpoint ~atts discharge l =
   let open DefAttributes in
-  let atts = parse atts in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  let do_cofixpoint = if Flags.is_program_mode () then
+  let do_cofixpoint = if atts.program then
       ComProgramFixpoint.do_cofixpoint
     else
       ComFixpoint.do_cofixpoint
@@ -1029,18 +1022,16 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 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
+  let program_mode = atts.program in
   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
+  Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
 
 let vernac_context ~poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
@@ -1572,14 +1563,6 @@ let () =
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
 
-let () =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "use of the program extension";
-      optkey   = ["Program";"Mode"];
-      optread  = (fun () -> !Flags.program_mode);
-      optwrite = (fun b -> Flags.program_mode:=b) }
-
 let () =
   declare_bool_option
     { optdepr  = false;
@@ -2189,6 +2172,11 @@ let with_module_locality ~atts f =
   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
+
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
@@ -2232,15 +2220,15 @@ let interp ?proof ~atts ~st c =
 
   (* Gallina *)
   | VernacDefinition ((discharge,kind),lid,d) ->
-      vernac_definition ~atts discharge kind lid d
-  | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l
+      with_def_attributes ~atts vernac_definition discharge kind lid d
+  | VernacStartTheoremProof (k,l) -> with_def_attributes vernac_start_proof ~atts k l
   | VernacEndProof e -> unsupported_attributes atts; vernac_end_proof ?proof e
   | VernacExactProof c -> unsupported_attributes atts; vernac_exact_proof c
   | VernacAssumption ((discharge,kind),nl,l) ->
-      vernac_assumption ~atts discharge kind l nl
+      with_def_attributes vernac_assumption ~atts discharge kind l nl
   | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l
-  | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l
-  | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l
+  | VernacFixpoint (discharge, l) -> with_def_attributes vernac_fixpoint ~atts discharge l
+  | VernacCoFixpoint (discharge, l) -> with_def_attributes vernac_cofixpoint ~atts discharge l
   | VernacScheme l -> unsupported_attributes atts; vernac_scheme l
   | VernacCombinedScheme (id, l) -> unsupported_attributes atts; vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe ~poly:(only_polymorphism atts) l
@@ -2271,9 +2259,9 @@ let interp ?proof ~atts ~st c =
 
   (* Type classes *)
   | VernacInstance (sup, inst, props, info) ->
-      vernac_instance ~atts sup inst props info
+      with_def_attributes vernac_instance ~atts sup inst props info
   | VernacDeclareInstance (sup, inst, info) ->
-      vernac_declare_instance ~atts sup inst info
+    with_def_attributes vernac_declare_instance ~atts sup inst info
   | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
   | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
   | VernacExistingClass id -> unsupported_attributes atts; vernac_existing_class id
@@ -2423,7 +2411,6 @@ let with_fail st b f =
   end
 
 let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
-  let orig_program_mode = Flags.is_program_mode () in
   let rec control = function
   | VernacExpr (atts, v) ->
     aux ~atts v
@@ -2445,21 +2432,13 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
       vernac_load control fname
 
     | c ->
-      let program = let open Attributes in
-        parse_drop_extra program_opt atts
-      in
       (* NB: we keep polymorphism and program in the attributes, we're
          just parsing them to do our option magic. *)
-      Option.iter Obligations.set_program_mode program;
       try
         vernac_timeout begin fun () ->
           if verbosely
           then Flags.verbosely (interp ?proof ~atts ~st) c
           else Flags.silently  (interp ?proof ~atts ~st) c;
-          (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
-             we should not restore the previous state of the flag... *)
-          if Option.has_some program then
-            Flags.program_mode := orig_program_mode;
           end
         with
         | reraise when
@@ -2470,7 +2449,6 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
             let e = CErrors.push reraise in
             let e = locate_if_not_already ?loc e in
             let () = restore_timeout () in
-            Flags.program_mode := orig_program_mode;
             iraise e
   in
   if verbosely