From 49a545b7606f8bd846d2e3740d0bb3ea1ea6eb38 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 17:47:03 +0100
Subject: 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.
---
 vernac/attributes.ml         | 16 ++++++++-
 vernac/attributes.mli        |  2 +-
 vernac/classes.ml            | 22 ++++++-------
 vernac/classes.mli           |  1 +
 vernac/comAssumption.ml      |  8 ++---
 vernac/comAssumption.mli     |  2 +-
 vernac/comDefinition.ml      | 18 +++++-----
 vernac/comDefinition.mli     |  2 +-
 vernac/comFixpoint.ml        | 24 +++++++-------
 vernac/comInductive.ml       |  6 ++--
 vernac/comProgramFixpoint.ml | 10 +++---
 vernac/declareDef.ml         |  2 +-
 vernac/lemmas.ml             |  8 ++---
 vernac/lemmas.mli            |  2 +-
 vernac/obligations.ml        | 10 +-----
 vernac/obligations.mli       |  2 +-
 vernac/record.ml             |  8 ++---
 vernac/vernacentries.ml      | 78 ++++++++++++++++----------------------------
 18 files changed, 104 insertions(+), 117 deletions(-)

(limited to 'vernac')

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
@@ -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
-- 
cgit v1.2.3