aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/attributes.ml16
-rw-r--r--vernac/attributes.mli6
-rw-r--r--vernac/auto_ind_decl.ml22
-rw-r--r--vernac/classes.ml3
-rw-r--r--vernac/comAssumption.ml4
-rw-r--r--vernac/comDefinition.ml27
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml8
-rw-r--r--vernac/comFixpoint.mli2
-rw-r--r--vernac/comInductive.ml14
-rw-r--r--vernac/declareDef.mli6
-rw-r--r--vernac/indschemes.ml4
-rw-r--r--vernac/lemmas.ml4
-rw-r--r--vernac/lemmas.mli2
-rw-r--r--vernac/metasyntax.ml94
-rw-r--r--vernac/metasyntax.mli10
-rw-r--r--vernac/obligations.ml14
-rw-r--r--vernac/obligations.mli5
-rw-r--r--vernac/record.ml16
-rw-r--r--vernac/vernacentries.ml31
-rw-r--r--vernac/vernacextend.ml19
-rw-r--r--vernac/vernacextend.mli13
22 files changed, 155 insertions, 167 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 1ad5862d5d..ab14974598 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -73,11 +73,6 @@ module Notations = struct
end
open Notations
-type deprecation = { since : string option ; note : string option }
-
-let mk_deprecation ?(since=None) ?(note=None) () =
- { since ; note }
-
let assert_empty k v =
if v <> VernacFlagEmpty
then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
@@ -213,19 +208,16 @@ let polymorphic =
universe_transform ~warn_unqualified:true >>
qualify_attribute ukey polymorphic_base
-let deprecation_parser : deprecation key_parser = fun orig args ->
+let deprecation_parser : Deprecation.t key_parser = fun orig args ->
assert_once ~name:"deprecation" orig;
match args with
| VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
| VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
- let since = Some since and note = Some note in
- mk_deprecation ~since ~note ()
+ Deprecation.make ~since ~note ()
| VernacFlagList [ "since", VernacFlagLeaf since ] ->
- let since = Some since in
- mk_deprecation ~since ()
+ Deprecation.make ~since ()
| VernacFlagList [ "note", VernacFlagLeaf note ] ->
- let note = Some note in
- mk_deprecation ~note ()
+ Deprecation.make ~note ()
| _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
let deprecation = attribute_of_list ["deprecated",deprecation_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 44688ddafc..53caf49efd 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -43,15 +43,11 @@ end
(** Definitions for some standard attributes. *)
-type deprecation = { since : string option ; note : string option }
-
-val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
-
val polymorphic : bool attribute
val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
-val deprecation : deprecation option attribute
+val deprecation : Deprecation.t option attribute
val canonical : bool attribute
val program_mode_option_name : string list
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5aec5cac2c..2e84c3275b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -195,7 +195,7 @@ let build_beq_scheme mode kn =
let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
match Constr.kind c with
- | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
+ | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects
| Var x ->
(* Support for working in a context with "eq_x : x -> x -> bool" *)
let eid = Id.of_string ("eq_"^(Id.to_string x)) in
@@ -203,11 +203,11 @@ let build_beq_scheme mode kn =
try ignore (Environ.lookup_named eid env)
with Not_found -> raise (ParameterWithoutEquality (VarRef x))
in
- mkVar eid, Safe_typing.empty_private_constants
+ mkVar eid, Evd.empty_side_effects
| Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
- if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
+ if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects
else begin
try
let eq, eff =
@@ -216,7 +216,7 @@ let build_beq_scheme mode kn =
let eqa, eff =
let eqa, effs = List.split (List.map aux a) in
Array.of_list eqa,
- List.fold_left Safe_typing.concat_private eff (List.rev effs)
+ List.fold_left Evd.concat_side_effects eff (List.rev effs)
in
let args =
Array.append
@@ -239,7 +239,7 @@ let build_beq_scheme mode kn =
let kneq = Constant.change_label kn eq_lbl in
try let _ = Environ.constant_opt_value_in env (kneq, u) in
Term.applist (mkConst kneq,a),
- Safe_typing.empty_private_constants
+ Evd.empty_side_effects
with Not_found -> raise (ParameterWithoutEquality (ConstRef kn)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
@@ -270,7 +270,7 @@ let build_beq_scheme mode kn =
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
let ar = Array.make n (ff ()) in
- let eff = ref Safe_typing.empty_private_constants in
+ let eff = ref Evd.empty_side_effects in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
let ar2 = Array.make n (ff ()) in
@@ -288,7 +288,7 @@ let build_beq_scheme mode kn =
(nb_cstr_args+ndx+1)
cc
in
- eff := Safe_typing.concat_private eff' !eff;
+ eff := Evd.concat_side_effects eff' !eff;
Array.set eqs ndx
(mkApp (eqA,
[|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -320,7 +320,7 @@ let build_beq_scheme mode kn =
let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
types = Array.make nb_ind mkSet and
cores = Array.make nb_ind mkSet in
- let eff = ref Safe_typing.empty_private_constants in
+ let eff = ref Evd.empty_side_effects in
let u = Univ.Instance.empty in
for i=0 to (nb_ind-1) do
names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
@@ -328,7 +328,7 @@ let build_beq_scheme mode kn =
(mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
let c, eff' = make_one_eq i in
cores.(i) <- c;
- eff := Safe_typing.concat_private eff' !eff
+ eff := Evd.concat_side_effects eff' !eff
done;
(Array.init nb_ind (fun i ->
let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
@@ -938,7 +938,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
Not_found ->
Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
end >>= fun (lbI,eff'') ->
- let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in
+ let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
Tacticals.New.tclTHENLIST [
Proofview.tclEFFECTS eff;
intros_using fresh_first_intros;
@@ -1005,7 +1005,7 @@ let make_eq_decidability mode mind =
(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
(compute_dec_tact ind lnamesparrec nparrec)
in
- ([|ans|], ctx), Safe_typing.empty_private_constants
+ ([|ans|], ctx), Evd.empty_side_effects
let eq_dec_scheme_kind =
declare_mutual_scheme_object "_eq_dec" make_eq_decidability
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 20402ebf95..178387dd17 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -532,8 +532,7 @@ let interp_instance_context ~program_mode env ctx ~generalize pl 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 imps = imps @ imps' in
let ctx', c = decompose_prod_assum sigma c' in
let ctx'' = ctx' @ ctx in
let (k, u), args = Typeclasses.dest_class_app (push_rel_context ctx'' env) sigma c in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 591e4b130f..a27c08d176 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -283,8 +283,8 @@ let context poly l =
Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
status
else
- let test (x, _) = match x with
- | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
+ let test x = match x.CAst.v with
+ | Some (Name id',_) -> Id.equal id id'
| _ -> false
in
let impl = List.exists test impls in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 4cae4b8a74..ae1f55acda 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -27,18 +27,19 @@ let warn_implicits_in_term =
CWarnings.create ~name:"implicits-in-term" ~category:"implicits"
(fun () ->
strbrk "Implicit arguments declaration relies on type." ++ spc () ++
- strbrk "The term declares more implicits than the type here.")
+ strbrk "Discarding incompatible declaration in term.")
let check_imps ~impsty ~impsbody =
- let b =
- try
- List.for_all (fun (key, (va:bool*bool*bool)) ->
- (* Pervasives.(=) is OK for this type *)
- Pervasives.(=) (List.assoc_f Constrexpr_ops.explicitation_eq key impsty) va)
- impsbody
- with Not_found -> false
- in
- if not b then warn_implicits_in_term ()
+ let rec aux impsty impsbody =
+ match impsty, impsbody with
+ | a1 :: impsty, a2 :: impsbody ->
+ (match a1.CAst.v, a2.CAst.v with
+ | None , None -> aux impsty impsbody
+ | Some _ , Some _ -> aux impsty impsbody
+ | _, _ -> warn_implicits_in_term ?loc:a2.CAst.loc ())
+ | _ :: _, [] | [], _ :: _ -> (* Information only on one side *) ()
+ | [], [] -> () in
+ aux impsty impsbody
let interp_definition ~program_mode pl bl poly red_option c ctypopt =
let env = Global.env() in
@@ -56,11 +57,11 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt =
match tyopt with
| None ->
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
+ evd, c, imps1@impsbody, None
| Some (ty, impsty) ->
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
+ evd, c, imps1@impsty, Some ty
in
(* Do the reduction *)
let evd, c = red_constant_body red_option env_bl evd c in
@@ -86,7 +87,7 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
if program_mode then
let env = Global.env () in
let (c,ctx), sideff = Future.force ce.const_entry_body in
- assert(Safe_typing.empty_private_constants = sideff);
+ assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
assert(Univ.ContextSet.is_empty ctx);
Obligations.check_evars env evd;
let c = EConstr.of_constr c in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index c3575594b6..0d9df47ee8 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -41,5 +41,5 @@ val interp_definition
-> red_expr option
-> constr_expr
-> constr_expr option
- -> Safe_typing.private_constants definition_entry *
+ -> Evd.side_effects definition_entry *
Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 3a25cb496c..0d7ba69955 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -197,7 +197,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
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
- (fun ctximps cclimps (_,ctx) -> ctximps@(Impargs.lift_implicits (Context.Rel.nhyps ctx) cclimps))
+ (fun ctximps cclimps (_,ctx) -> ctximps@cclimps)
fixctximps fixcclimps fixctxs in
let sigma, rec_sign =
List.fold_left2
@@ -286,7 +286,8 @@ let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximp
let evd = Evd.restrict_universe_context evd vars in
let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
- let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+ let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
+ let fixdecls = List.map mk_pure fixdecls in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
@@ -316,7 +317,8 @@ let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fixi
let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
let vars = Vars.universes_of_constr (List.hd fixdecls) in
- let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
+ let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
+ let fixdecls = List.map mk_pure fixdecls in
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a31f3c34e0..1ded9f3d29 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -57,7 +57,7 @@ val interp_recursive :
(* names / defs / types *)
(Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
(* ctx per mutual def / implicits / struct annotations *)
- (EConstr.rel_context * Impargs.manual_explicitation list * int option) list
+ (EConstr.rel_context * Impargs.manual_implicits * int option) list
(** Exported for Funind *)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5bebf955ec..2f8b12f4c5 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -375,8 +375,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
(* Compute interpretation metadatas *)
- let indimpls = List.map (fun impls -> userimpls @
- lift_implicits (Context.Rel.nhyps ctx_params) impls) indimpls in
+ let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data sigma env_params params) arities indnames in
@@ -402,8 +401,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
constructors
in
let ctx_params = ctx_params @ ctx_uparams in
- let userimpls = useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) userimpls) in
- let indimpls = List.map (fun iimpl -> useruimpls @ (lift_implicits (Context.Rel.nhyps ctx_uparams) iimpl)) indimpls in
+ let userimpls = useruimpls @ userimpls in
+ let indimpls = List.map (fun iimpl -> useruimpls @ iimpl) indimpls in
let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in
let env_ar = push_types env0 indnames relevances fullarities in
let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
@@ -450,10 +449,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
indl arities arityconcl constructors
in
let impls =
- let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
indimpls, List.map (fun impls ->
- userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
+ userimpls @ impls) cimpls) indimpls constructors
in
let variance = if poly && cum then Some (InferCumulativity.dummy_variance uctx) else None in
(* Build the mutual inductive entry *)
@@ -559,8 +557,8 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
mind
type one_inductive_impls =
- Impargs.manual_explicitation list (* for inds *)*
- Impargs.manual_explicitation list list (* for constrs *)
+ Impargs.manual_implicits (* for inds *) *
+ Impargs.manual_implicits list (* for constrs *)
type uniform_inductive_flag =
| UniformParameters
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 2b9d9567cd..909aa41a30 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,7 +15,7 @@ val declare_definition
: Id.t
-> definition_kind
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
- -> Safe_typing.private_constants Entries.definition_entry
+ -> Evd.side_effects Entries.definition_entry
-> UnivNames.universe_binders
-> Impargs.manual_implicits
-> GlobRef.t
@@ -27,7 +27,7 @@ val declare_fix
-> UnivNames.universe_binders
-> Entries.universes_entry
-> Id.t
- -> Safe_typing.private_constants Entries.proof_output
+ -> Evd.side_effects Entries.proof_output
-> Constr.types
-> Impargs.manual_implicits
-> GlobRef.t
@@ -36,7 +36,7 @@ val prepare_definition : allow_evars:bool ->
?opaque:bool -> ?inline:bool -> poly:bool ->
Evd.evar_map -> UState.universe_decl ->
types:EConstr.t option -> body:EConstr.t ->
- Evd.evar_map * Safe_typing.private_constants Entries.definition_entry
+ Evd.evar_map * Evd.side_effects Entries.definition_entry
val prepare_parameter : allow_evars:bool ->
poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index de7d2fd49a..f18cf17bf9 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -414,7 +414,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
let decltype = EConstr.to_constr sigma decltype in
- let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in
ConstRef cst :: lrecref
in
@@ -536,7 +536,7 @@ let do_combined_scheme name schemes =
schemes
in
let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
- let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
(* It is possible for the constants to have different universe
polymorphism from each other, however that is only when the user
manually defined at least one of them (as Scheme would pick the
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4e346a9564..7aba64fb93 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -112,7 +112,7 @@ let adjust_guardness_conditions const = function
List.interval 0 (List.length ((lam_assum c))))
lemma_guard (Array.to_list fixdefs) in
*)
- let env = Safe_typing.push_private_constants env eff in
+ let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
let indexes =
search_guard env
possible_indexes fixdecls in
@@ -469,7 +469,7 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
(* XXX: The nf_evar is critical !! *)
evd, (id.CAst.v,
(Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
- (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps'))))
+ (ids, imps @ imps'))))
evd thms in
let recguard,thms,snl = look_for_possibly_mutual_statements evd thms in
let evd = Evd.minimize_universes evd in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index ac647af8b5..25c5b24e91 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -112,7 +112,7 @@ val start_lemma_with_initialization
-> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
-> (Id.t (* name of thm *) *
(EConstr.types (* type of thm *) *
- (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
+ (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
-> int list option
-> t
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 50914959dc..b96f500beb 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -732,13 +732,8 @@ type syntax_extension = {
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
synext_extra : (string * string) list;
- synext_compat : Flags.compat_version option;
}
-let is_active_compat = function
-| None -> true
-| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
-
type syntax_extension_obj = locality_flag * syntax_extension
let check_and_extend_constr_grammar ntn rule =
@@ -759,7 +754,7 @@ let cache_one_syntax_extension se =
let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
with Not_found ->
- if is_active_compat se.synext_compat then begin
+ begin
(* Reserve the notation level *)
Notgram_ops.declare_notation_level ntn prec ~onlyprint;
(* Declare the parsing rule *)
@@ -934,10 +929,6 @@ let is_only_printing mods =
let test = function SetOnlyPrinting -> true | _ -> false in
List.exists test mods
-let get_compat_version mods =
- let test = function SetCompatVersion v -> Some v | _ -> None in
- try Some (List.find_map test mods) with Not_found -> None
-
(* Compute precedences from modifiers (or find default ones) *)
let set_entry_type from etyps (x,typ) =
@@ -1177,7 +1168,7 @@ module SynData = struct
(* Fields coming from the vernac-level modifiers *)
only_parsing : bool;
only_printing : bool;
- compat : Flags.compat_version option;
+ deprecation : Deprecation.t option;
format : lstring option;
extra : (string * string) list;
@@ -1222,12 +1213,32 @@ let check_locality_compatibility local custom i_typs =
strbrk " which is local."))
(List.uniquize allcustoms)
-let compute_syntax_data local df modifiers =
+let warn_deprecated_compat =
+ CWarnings.create ~name:"deprecated-compat" ~category:"deprecated"
+ (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++
+ str"Please use the \"deprecated\" attributed instead."))
+
+(* Returns the new deprecation and the onlyparsing status. This should be
+removed together with the compat syntax modifier. *)
+let merge_compat_deprecation compat deprecation =
+ match compat, deprecation with
+ | Some Flags.Current, _ -> deprecation, true
+ | Some _, Some _ ->
+ CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute."
+ ++ spc () ++ str"Please use only the latter.")
+ | Some v, None ->
+ warn_deprecated_compat ();
+ Some (Deprecation.make ~since:(Flags.pr_version v) ()), true
+ | None, Some _ -> deprecation, true
+ | None, None -> deprecation, false
+
+let compute_syntax_data ~local deprecation df modifiers =
let open SynData in
let open NotationMods in
let mods = interp_modifiers modifiers in
let onlyprint = mods.only_printing in
let onlyparse = mods.only_parsing in
+ let deprecation, _ = merge_compat_deprecation mods.compat deprecation in
if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
@@ -1265,7 +1276,7 @@ let compute_syntax_data local df modifiers =
only_parsing = mods.only_parsing;
only_printing = mods.only_printing;
- compat = mods.compat;
+ deprecation;
format = mods.format;
extra = mods.extra;
@@ -1281,9 +1292,9 @@ let compute_syntax_data local df modifiers =
not_data = sy_fulldata;
}
-let compute_pure_syntax_data local df mods =
+let compute_pure_syntax_data ~local df mods =
let open SynData in
- let sd = compute_syntax_data local df mods in
+ let sd = compute_syntax_data ~local None df mods in
let msgs =
if sd.only_parsing then
(Feedback.msg_warning ?loc:None,
@@ -1301,7 +1312,7 @@ type notation_obj = {
notobj_coercion : entry_coercion_kind option;
notobj_onlyparse : bool;
notobj_onlyprint : bool;
- notobj_compat : Flags.compat_version option;
+ notobj_deprecation : Deprecation.t option;
notobj_notation : notation * notation_location;
}
@@ -1323,11 +1334,11 @@ let open_notation i (_, nobj) =
let (ntn, df) = nobj.notobj_notation in
let pat = nobj.notobj_interp in
let onlyprint = nobj.notobj_onlyprint in
+ let deprecation = nobj.notobj_deprecation in
let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
- let active = is_active_compat nobj.notobj_compat in
- if Int.equal i 1 && fresh && active then begin
+ if Int.equal i 1 && fresh then begin
(* Declare the interpretation *)
- let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
+ let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
(* Declare the uninterpretation *)
if not nobj.notobj_onlyparse then
Notation.declare_uninterpretation (NotationRule (scope, ntn)) pat;
@@ -1388,7 +1399,6 @@ let recover_notation_syntax ntn =
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
synext_extra = pp_extra_rules;
- synext_compat = None;
}
with Not_found ->
raise NoSyntaxRule
@@ -1437,7 +1447,6 @@ let make_syntax_rules (sd : SynData.syn_data) = let open SynData in
synext_notgram = { notgram_onlyprinting = sd.only_printing; notgram_rules = pa_rule };
synext_unparsing = pp_rule;
synext_extra = sd.extra;
- synext_compat = sd.compat;
}
(**********************************************************************)
@@ -1447,9 +1456,9 @@ let to_map l =
let fold accu (x, v) = Id.Map.add x v accu in
List.fold_left fold Id.Map.empty l
-let add_notation_in_scope local df env c mods scope =
+let add_notation_in_scope ~local deprecation df env c mods scope =
let open SynData in
- let sd = compute_syntax_data local df mods in
+ let sd = compute_syntax_data ~local deprecation df mods in
(* Prepare the interpretation *)
(* Prepare the parsing and printing rules *)
let sy_rules = make_syntax_rules sd in
@@ -1470,7 +1479,7 @@ let add_notation_in_scope local df env c mods scope =
notobj_onlyparse = onlyparse;
notobj_coercion = coe;
notobj_onlyprint = sd.only_printing;
- notobj_compat = sd.compat;
+ notobj_deprecation = sd.deprecation;
notobj_notation = sd.info;
} in
(* Ready to change the global state *)
@@ -1479,7 +1488,7 @@ let add_notation_in_scope local df env c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
sd.info
-let add_notation_interpretation_core local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
+let add_notation_interpretation_core ~local df env ?(impls=empty_internalization_env) c scope onlyparse onlyprint deprecation =
let (recvars,mainvars,symbs) = analyze_notation_tokens ~onlyprint df in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
let level, i_typs, onlyprint = if not (is_numeral symbs) then begin
@@ -1510,7 +1519,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
notobj_onlyparse = onlyparse;
notobj_coercion = coe;
notobj_onlyprint = onlyprint;
- notobj_compat = compat;
+ notobj_deprecation = deprecation;
notobj_notation = df';
} in
Lib.add_anonymous_leaf (inNotation notation);
@@ -1518,41 +1527,40 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_
(* Notations without interpretation (Reserved Notation) *)
-let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in
- let psd = compute_pure_syntax_data local df mods in
- let sy_rules = make_syntax_rules {psd with compat = None} in
+let add_syntax_extension ~local ({CAst.loc;v=df},mods) = let open SynData in
+ let psd = compute_pure_syntax_data ~local df mods in
+ let sy_rules = make_syntax_rules {psd with deprecation = None} in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
(* Notations with only interpretation *)
let add_notation_interpretation env ({CAst.loc;v=df},c,sc) =
- let df' = add_notation_interpretation_core false df env c sc false false None in
+ let df' = add_notation_interpretation_core ~local:false df env c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) =
(try ignore
- (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ());
+ (Flags.silently (fun () -> add_notation_interpretation_core ~local:false df env ~impls c sc false false None) ());
with NoSyntaxRule ->
user_err Pp.(str "Parsing rule for this notation has to be previously declared."));
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
(* Main entry point *)
-let add_notation local env c ({CAst.loc;v=df},modifiers) sc =
+let add_notation ~local deprecation env c ({CAst.loc;v=df},modifiers) sc =
let df' =
if no_syntax_modifiers modifiers then
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
let onlyprint = is_only_printing modifiers in
- let compat = get_compat_version modifiers in
- try add_notation_interpretation_core local df env c sc onlyparse onlyprint compat
+ try add_notation_interpretation_core ~local df env c sc onlyparse onlyprint deprecation
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
- add_notation_in_scope local df env c modifiers sc
+ add_notation_in_scope ~local deprecation df env c modifiers sc
else
(* Declare both syntax and interpretation *)
- add_notation_in_scope local df env c modifiers sc
+ add_notation_in_scope ~local deprecation df env c modifiers sc
in
Dumpglob.dump_notation (loc,df') sc true
@@ -1566,7 +1574,7 @@ let add_notation_extra_printing_rule df k v =
let inject_var x = CAst.make @@ CRef (qualid_of_ident x,None)
-let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
+let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc =
check_infix_modifiers modifiers;
(* check the precedence *)
let vars = names_of_constr_expr pr in
@@ -1575,7 +1583,7 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
let metas = [inject_var x; inject_var y] in
let c = mkAppC (pr,metas) in
let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in
- add_notation local env c (df,modifiers) sc
+ add_notation ~local deprecation env c (df,modifiers) sc
(**********************************************************************)
(* Scopes, delimiters and classes bound to scopes *)
@@ -1651,7 +1659,7 @@ let try_interp_name_alias = function
| [], { CAst.v = CRef (ref,_) } -> intern_reference ref
| _ -> raise Not_found
-let add_syntactic_definition env ident (vars,c) local onlyparse =
+let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
let vars,reversibility,pat =
try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
with Not_found ->
@@ -1665,11 +1673,9 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
List.map map vars, reversibility, pat
in
- let onlyparse = match onlyparse with
- | None when fst (printability None false reversibility pat) -> Some Flags.Current
- | p -> p
- in
- Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
+ let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in
+ let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
+ Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
(**********************************************************************)
(* Declaration of custom entry *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 6435df23c7..6532cee367 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -19,10 +19,10 @@ val add_token_obj : string -> unit
(** Adding a (constr) notation in the environment*)
-val add_infix : locality_flag -> env -> (lstring * syntax_modifier list) ->
+val add_infix : local:bool -> Deprecation.t option -> env -> (lstring * syntax_modifier list) ->
constr_expr -> scope_name option -> unit
-val add_notation : locality_flag -> env -> constr_expr ->
+val add_notation : local:bool -> Deprecation.t option -> env -> constr_expr ->
(lstring * syntax_modifier list) -> scope_name option -> unit
val add_notation_extra_printing_rule : string -> string -> string -> unit
@@ -47,12 +47,12 @@ val set_notation_for_interpretation : env -> Constrintern.internalization_env ->
(** Add only the parsing/printing rule of a notation *)
val add_syntax_extension :
- locality_flag -> (lstring * syntax_modifier list) -> unit
+ local:bool -> (lstring * syntax_modifier list) -> unit
(** Add a syntactic definition (as in "Notation f := ...") *)
-val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr ->
- bool -> Flags.compat_version option -> unit
+val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
+ Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
(** Print the Camlp5 state of a grammar *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6c9ec95c5f..6ef2f80067 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -307,7 +307,7 @@ type program_info_aux = {
prg_obligations: obligations;
prg_deps : Id.t list;
prg_fixkind : fixpoint_kind option ;
- prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
+ prg_implicits : Impargs.manual_implicits;
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
@@ -497,7 +497,7 @@ let compute_possible_guardness_evidences n fixbody fixtype =
let ctx = fst (decompose_prod_n_assum m fixtype) in
List.map_i (fun i _ -> i) 0 ctx
-let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants)
+let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
let declare_mutual_definition l =
let len = List.length l in
@@ -632,7 +632,7 @@ let declare_obligation prg obl body ty uctx =
if get_shrink_obligations () && not poly then
shrink_body body ty else [], body, ty, [||]
in
- let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+ let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in
let ce =
{ const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
const_entry_secctx = None;
@@ -822,8 +822,8 @@ let solve_by_tac ?loc name evi t poly ctx =
Pfedit.build_constant_by_tactic
id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in
let env = Global.env () in
- let body = Future.force entry.const_entry_body in
- let body = Safe_typing.inline_private_constants env body in
+ let (body, eff) = Future.force entry.const_entry_body in
+ let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx')
@@ -848,8 +848,8 @@ let obligation_terminator ?hook name num guard auto pf =
| Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
let env = Global.env () in
let ty = entry.Entries.const_entry_type in
- let body = Future.force entry.const_entry_body in
- let (body, cstr) = Safe_typing.inline_private_constants env body in
+ let body, eff = Future.force entry.const_entry_body in
+ let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
let sigma = Evd.from_ctx uctx in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 8734d82970..18a7e10733 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -57,7 +57,7 @@ val add_definition
-> ?term:constr -> types
-> UState.t
-> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
- -> ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list
+ -> ?implicits:Impargs.manual_implicits
-> ?kind:Decl_kinds.definition_kind
-> ?tactic:unit Proofview.tactic
-> ?reduce:(constr -> constr)
@@ -74,8 +74,7 @@ type fixpoint_kind =
| IsCoFixpoint
val add_mutual_definitions :
- (Names.Id.t * constr * types *
- (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
+ (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list ->
UState.t ->
?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
?tactic:unit Proofview.tactic ->
diff --git a/vernac/record.ml b/vernac/record.ml
index 6101e13edd..48cde133a8 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -344,7 +344,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
try
let entry = {
const_entry_body =
- Future.from_val (Safe_typing.mk_pure_proof proj);
+ Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_universes = ctx;
@@ -476,21 +476,15 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
List.mapi map record_data
let implicits_of_context ctx =
- List.map_i (fun i name ->
- let explname =
- match name with
- | Name n -> Some n
- | Anonymous -> None
- in ExplByPos (i, explname), (true, true, true))
- 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
+ List.map (fun name -> CAst.make (Some (name,true)))
+ (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
let declare_class def cum ubinders univs id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) coers priorities =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
- let len = List.length params in
let impls = implicits_of_context params in
- List.map (fun x -> impls @ Impargs.lift_implicits (succ len) x) fieldimpls
+ List.map (fun x -> impls @ x) fieldimpls
in
let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
let data =
@@ -704,7 +698,7 @@ let definition_structure udecl kind ~template cum poly finite records =
declare_class def cum ubinders univs id.CAst.v idbuild
implpars params arity template implfs fields coers priorities
| _ ->
- let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
+ let map impls = implpars @ [CAst.make None] @ impls in
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d206165e88..112c4b6451 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -81,7 +81,7 @@ module DefAttributes = struct
locality : bool option;
polymorphic : bool;
program : bool;
- deprecated : deprecation option;
+ deprecated : Deprecation.t option;
}
let parse f =
@@ -92,6 +92,8 @@ module DefAttributes = struct
{ polymorphic; program; locality; deprecated }
end
+let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
+
let with_locality ~atts f =
let local = Attributes.(parse locality atts) in
f ~local
@@ -102,8 +104,7 @@ let with_section_locality ~atts f =
f ~section_local
let with_module_locality ~atts f =
- let local = Attributes.(parse locality atts) in
- let module_local = make_module_locality local in
+ let module_local = Attributes.(parse module_locality atts) in
f ~module_local
let with_def_attributes ~atts f =
@@ -504,7 +505,7 @@ let dump_global r =
let vernac_syntax_extension ~module_local infix l =
if infix then Metasyntax.check_infix_modifiers (snd l);
- Metasyntax.add_syntax_extension module_local l
+ Metasyntax.add_syntax_extension ~local:module_local l
let vernac_declare_scope ~module_local sc =
Metasyntax.declare_scope module_local sc
@@ -523,11 +524,13 @@ let vernac_open_close_scope ~section_local (b,s) =
let vernac_arguments_scope ~section_local r scl =
Notation.declare_arguments_scope section_local (smart_global r) scl
-let vernac_infix ~module_local =
- Metasyntax.add_infix module_local (Global.env())
+let vernac_infix ~atts =
+ let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+ Metasyntax.add_infix ~local:module_local deprecation (Global.env())
-let vernac_notation ~module_local =
- Metasyntax.add_notation module_local (Global.env())
+let vernac_notation ~atts =
+ let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
+ Metasyntax.add_notation ~local:module_local deprecation (Global.env())
let vernac_custom_entry ~module_local s =
Metasyntax.declare_custom_entry module_local s
@@ -1265,9 +1268,10 @@ let vernac_hints ~atts dbnames h =
let local = enforce_module_locality local in
Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
-let vernac_syntactic_definition ~module_local lid x y =
+let vernac_syntactic_definition ~atts lid x compat =
+ let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
Dumpglob.dump_definition lid false "syndef";
- Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
+ Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
let cache_bidi_hints (_name, (gr, ohint)) =
match ohint with
@@ -2379,9 +2383,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
| VernacOpenCloseScope (b, s) ->
VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s))
| VernacInfix (mv,qid,sc) ->
- VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc)
+ VtDefault(fun () -> vernac_infix ~atts mv qid sc)
| VernacNotation (c,infpl,sc) ->
- VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc)
+ VtDefault(fun () -> vernac_notation ~atts c infpl sc)
| VernacNotationAddFormat(n,k,v) ->
VtDefault(fun () ->
unsupported_attributes atts;
@@ -2559,8 +2563,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
VtDefault(fun () ->
vernac_hints ~atts dbnames hints)
| VernacSyntacticDefinition (id,c,b) ->
- VtDefault(fun () ->
- with_module_locality ~atts vernac_syntactic_definition id c b)
+ VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
| VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
VtDefault(fun () ->
with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 6a52177dd5..c7008c2a84 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -16,7 +16,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
-type vernac_type =
+type vernac_when =
+ | VtNow
+ | VtLater
+
+type vernac_classification =
(* Start of a proof *)
| VtStartProof of vernac_start
(* Command altering the global state, bad for parallel
@@ -37,7 +41,7 @@ type vernac_type =
(* To be removed *)
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -48,11 +52,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
-type vernac_when =
- | VtNow
- | VtLater
-type vernac_classification = vernac_type * vernac_when
-
type typed_vernac =
| VtDefault of (unit -> unit)
@@ -130,9 +129,9 @@ let get_vernac_classifier (name, i) args =
let declare_vernac_classifier name f =
classifiers := String.Map.add name f !classifiers
-let classify_as_query = VtQuery, VtLater
-let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
+let classify_as_query = VtQuery
+let classify_as_sideeff = VtSideff ([], VtLater)
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}
type (_, _) ty_sig =
| TyNil : (vernac_command, vernac_classification) ty_sig
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 78b7f21b0d..fd59d77237 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -32,7 +32,11 @@ type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = VtKeep of vernac_keep_as | VtDrop
-type vernac_type =
+type vernac_when =
+ | VtNow
+ | VtLater
+
+type vernac_classification =
(* Start of a proof *)
| VtStartProof of vernac_start
(* Command altering the global state, bad for parallel
@@ -53,7 +57,7 @@ type vernac_type =
(* To be removed *)
| VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
-and vernac_sideff_type = Names.Id.t list
+and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
| GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
| Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
@@ -64,11 +68,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)
and proof_block_name = string (** open type of delimiters *)
-type vernac_when =
- | VtNow
- | VtLater
-type vernac_classification = vernac_type * vernac_when
-
(** Interpretation of extended vernac phrases. *)
type typed_vernac =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 18:23:32 +0000