Make Program a regular attribute

We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.

This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.

18 files changed, 104 insertions, 117 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 4f238f38e6..9b8c4efb37 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 66e10f94cd..3cb4d69ca0 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 dd49f09d35..ea434dbc4f 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 6f61da66cf..7e0ec42625 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 7301e1fff7..73d0be04df 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 c5bf3725a9..385ec33bea 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 79d45880fc..5e74114a86 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 0ac5762f71..9cb6190fcc 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 77227b64e6..5229d9e8e8 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 afee2a5868..68ad276113 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 edce8e255c..a30313d37c 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 41057f8ab2..361ed1a737 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 0dfbba0e83..4635883dc2 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 3ac12d3b0b..a9a10a6e38 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 6642d04c98..6014452107 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 c670e3a3b5..4eef668f56 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 1b7b828f47..247e0790d7 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 7611355100..eb263757e2 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
@@ -1575,14 +1566,6 @@ let () =
 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;
       optname  = "Polymorphic inductive cumulativity";
       optkey   = ["Polymorphic"; "Inductive"; "Cumulativity"];
       optread  = Flags.is_polymorphic_inductive_cumulativity;
@@ -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