aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml16
-rw-r--r--vernac/attributes.mli2
-rw-r--r--vernac/classes.ml22
-rw-r--r--vernac/classes.mli1
-rw-r--r--vernac/comAssumption.ml8
-rw-r--r--vernac/comAssumption.mli2
-rw-r--r--vernac/comDefinition.ml18
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml24
-rw-r--r--vernac/comInductive.ml6
-rw-r--r--vernac/comProgramFixpoint.ml10
-rw-r--r--vernac/declareDef.ml2
-rw-r--r--vernac/lemmas.ml8
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/obligations.ml10
-rw-r--r--vernac/obligations.mli2
-rw-r--r--vernac/record.ml8
-rw-r--r--vernac/vernacentries.ml78
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 02:17:01 +0000