aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/canonical.ml15
-rw-r--r--vernac/canonical.mli2
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comAssumption.ml27
-rw-r--r--vernac/comInductive.ml64
-rw-r--r--vernac/comInductive.mli58
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declaremods.ml22
-rw-r--r--vernac/egramcoq.ml12
-rw-r--r--vernac/g_vernac.mlg34
-rw-r--r--vernac/himsg.ml14
-rw-r--r--vernac/indschemes.ml18
-rw-r--r--vernac/metasyntax.ml30
-rw-r--r--vernac/metasyntax.mli2
-rw-r--r--vernac/ppvernac.ml11
-rw-r--r--vernac/prettyp.ml6
-rw-r--r--vernac/record.ml29
-rw-r--r--vernac/vernacentries.ml29
-rw-r--r--vernac/vernacexpr.ml4
20 files changed, 178 insertions, 207 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 310ea62a1d..f954915cf8 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -430,7 +430,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
end
(* used in the bool -> leb side *)
-let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
+let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let open EConstr in
let avoid = Array.of_list aavoid in
let do_arg sigma hd v offset =
@@ -658,7 +658,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
then
Tacticals.New.tclTHEN
- (do_replace_bl mode bl_scheme_key ind
+ (do_replace_bl bl_scheme_key ind
(!avoid)
nparrec (ca.(2))
(ca.(1)))
diff --git a/vernac/canonical.ml b/vernac/canonical.ml
index e9454bab8a..141b02ef63 100644
--- a/vernac/canonical.ml
+++ b/vernac/canonical.ml
@@ -11,29 +11,30 @@ open Names
open Libobject
open Recordops
-let open_canonical_structure i (_, o) =
+let open_canonical_structure i (_, (o,_)) =
let env = Global.env () in
let sigma = Evd.from_env env in
if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
-let cache_canonical_structure (_, o) =
+let cache_canonical_structure (_, (o,_)) =
let env = Global.env () in
let sigma = Evd.from_env env in
register_canonical_structure ~warn:true env sigma o
-let discharge_canonical_structure (_,x) = Some x
+let discharge_canonical_structure (_,(x, local)) =
+ if local then None else Some (x, local)
-let inCanonStruc : Constant.t * inductive -> obj =
+let inCanonStruc : (Constant.t * inductive) * bool -> obj =
declare_object {(default_object "CANONICAL-STRUCTURE") with
open_function = open_canonical_structure;
cache_function = cache_canonical_structure;
- subst_function = (fun (subst,c) -> subst_canonical_structure subst c);
+ subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local);
classify_function = (fun x -> Substitute x);
discharge_function = discharge_canonical_structure }
let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
-let declare_canonical_structure ref =
+let declare_canonical_structure ?(local=false) ref =
let env = Global.env () in
let sigma = Evd.from_env env in
- add_canonical_structure (check_and_decompose_canonical_structure env sigma ref)
+ add_canonical_structure (check_and_decompose_canonical_structure env sigma ref, local)
diff --git a/vernac/canonical.mli b/vernac/canonical.mli
index a3bbaf6d18..e4161b4f97 100644
--- a/vernac/canonical.mli
+++ b/vernac/canonical.mli
@@ -9,4 +9,4 @@
(************************************************************************)
open Names
-val declare_canonical_structure : GlobRef.t -> unit
+val declare_canonical_structure : ?local:bool -> GlobRef.t -> unit
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 0333b73ffe..c9b5144299 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -410,7 +410,7 @@ let do_instance_resolve_TC termtype sigma env =
(* Beware of this step, it is required as to minimize universes. *)
let sigma = Evd.minimize_universes sigma in
(* Check that the type is free of evars now. *)
- Pretyping.check_evars env (Evd.from_env env) sigma termtype;
+ Pretyping.check_evars env sigma termtype;
termtype, sigma
let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst =
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e5db6146ca..8a403e5a03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -22,24 +22,6 @@ open Entries
module RelDecl = Context.Rel.Declaration
(* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
-let axiom_into_instance = ref false
-
-let () =
- let open Goptions in
- declare_bool_option
- { optdepr = true;
- optname = "automatically declare axioms whose type is a typeclass as instances";
- optkey = ["Typeclasses";"Axioms";"Are";"Instances"];
- optread = (fun _ -> !axiom_into_instance);
- optwrite = (:=) axiom_into_instance; }
-
-let should_axiom_into_instance = let open Decls in function
- | Context ->
- (* The typeclass behaviour of Variable and Context doesn't depend
- on section status *)
- true
- | Definitional | Logical | Conjectural -> !axiom_into_instance
-
let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
let kind = Decls.IsAssumption kind in
let decl = Declare.SectionLocalAssum {typ; impl} in
@@ -58,7 +40,12 @@ let instance_of_univ_entry = function
| Monomorphic_entry _ -> Univ.Instance.empty
let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name} =
- let do_instance = should_axiom_into_instance kind in
+ let do_instance = let open Decls in match kind with
+ | Context -> true
+ (* The typeclass behaviour of Variable and Context doesn't depend
+ on section status *)
+ | Definitional | Logical | Conjectural -> false
+ in
let inl = let open Declaremods in match nl with
| NoInline -> None
| DefaultInline -> Some (Flags.get_inline_level())
@@ -268,7 +255,7 @@ let context ~poly l =
let sigma, (_, ((_env, ctx), 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
+ let ce t = Pretyping.check_evars env sigma t in
let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) ctx in
(* reorder, evar-normalize and add implicit status *)
let ctx = List.rev_map (fun d ->
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 80fcb7bc45..b603c54026 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -255,7 +255,7 @@ let inductive_levels env evd arities inds =
in
let cstrs_levels, min_levels, sizes =
CList.split3
- (List.map2 (fun (_,tys,_) (arity,(ctx,du)) ->
+ (List.map2 (fun (_,tys) (arity,(ctx,du)) ->
let len = List.length tys in
let minlev = Sorts.univ_of_sort du in
let minlev =
@@ -323,16 +323,18 @@ let check_named {CAst.loc;v=na} = match na with
let msg = str "Parameters must be named." in
user_err ?loc msg
-let template_polymorphism_candidate env uctx params concl =
+let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl =
match uctx with
| Entries.Monomorphic_entry uctx ->
let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
if not concltemplate then false
+ else if not template_check then true
else
- let template_check = Environ.check_template env in
let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
- let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in
- not (template_check && Univ.LSet.is_empty conclunivs)
+ let params, conclunivs =
+ IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu
+ in
+ not (Univ.LSet.is_empty conclunivs)
| Entries.Polymorphic_entry _ -> false
let check_param = function
@@ -348,42 +350,47 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
let uvars = Univ.LSet.empty in
let uvars = Context.Rel.(fold_outside (Declaration.fold_constr merge_universes_of_constr) ctx_params ~init:uvars) in
let uvars = List.fold_right merge_universes_of_constr arities uvars in
- let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
+ let uvars = List.fold_right (fun (_,ctypes) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
Evd.restrict_universe_context sigma uvars
-let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
+let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite =
(* Compute renewed arities *)
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
- let constructors = List.map (on_pi2 (List.map nf)) constructors in
+ let constructors = List.map (on_snd (List.map nf)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let arities = List.map (on_snd nf) arities in
- let constructors = List.map (on_pi2 (List.map nf)) constructors in
+ let constructors = List.map (on_snd (List.map nf)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
let uctx = Evd.check_univ_decl ~poly sigma udecl in
- List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
- Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
- List.iter (fun (_,ctyps,_) ->
- List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
- constructors;
(* Build the inductive entries *)
- let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+ let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
let template_candidate () =
- templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in
+ templatearity ||
+ let ctor_levels =
+ let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+ let param_levels =
+ List.fold_left (fun levels d -> match d with
+ | LocalAssum _ -> levels
+ | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+ Univ.LSet.empty ctx_params
+ in
+ List.fold_left (fun levels c -> add_levels c levels)
+ param_levels ctypes
+ in
+ template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl
+ in
let template = match template with
| Some template ->
if poly && template then user_err
Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
- if template && not (template_candidate ()) then
- user_err Pp.(strbrk "Inductive " ++ Id.print indname ++
- str" cannot be made template polymorphic.");
template
| None ->
should_auto_template indname (template_candidate ())
@@ -396,7 +403,6 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
})
indnames arities arityconcl constructors
in
- let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in
(* Build the mutual inductive entry *)
let mind_ent =
{ mind_entry_params = ctx_params;
@@ -405,12 +411,10 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
mind_entry_inds = entries;
mind_entry_private = if private_ind then Some false else None;
mind_entry_universes = uctx;
- mind_entry_variance = variance;
+ mind_entry_cumulative = poly && cumulative;
}
in
- (if poly && cumulative then
- InferCumulativity.infer_inductive env_ar mind_ent
- else mind_ent), Evd.universe_binders sigma
+ mind_ent, Evd.universe_binders sigma
let interp_params env udecl uparamsl paramsl =
let sigma, udecl = interp_univ_decl_opt env udecl in
@@ -480,9 +484,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
List.init (List.length indl) EConstr.(fun i -> mkApp (mkRel (i + 1 + nuparams), uargs))
@ List.init nuparams EConstr.(fun i -> mkRel (i + 1)) in
let generalize_constructor c = EConstr.Unsafe.to_constr (EConstr.Vars.substnl uparam_subst nparams c) in
+ let cimpls = List.map pi3 constructors in
let constructors = List.map (fun (cnames,ctypes,cimpls) ->
- (cnames,List.map generalize_constructor ctypes,cimpls))
- constructors
+ (cnames,List.map generalize_constructor ctypes))
+ constructors
in
let ctx_params = ctx_params @ ctx_uparams in
let userimpls = useruimpls @ userimpls in
@@ -493,11 +498,12 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
(* Try further to solve evars, and instantiate them *)
let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in
let impls =
- List.map2 (fun indimpls (_,_,cimpls) ->
+ List.map2 (fun indimpls cimpls ->
indimpls, List.map (fun impls ->
- userimpls @ impls) cimpls) indimpls constructors
+ userimpls @ impls) cimpls)
+ indimpls cimpls
in
- let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
+ let mie, pl = interp_mutual_inductive_constr ~template ~sigma ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in
(mie, pl, impls)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 45e539b1e4..cc104b3762 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -49,24 +49,22 @@ val declare_mutual_inductive_with_eliminations
-> Names.MutInd.t
[@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
-val interp_mutual_inductive_constr :
- env0:Environ.env ->
- sigma:Evd.evar_map ->
- template:bool option ->
- udecl:UState.universe_decl ->
- env_ar:Environ.env ->
- env_params:Environ.env ->
- ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list ->
- indnames:Names.Id.t list ->
- arities:EConstr.t list ->
- arityconcl:(bool * EConstr.ESorts.t) option list ->
- constructors:(Names.Id.t list * Constr.constr list * 'a list list) list ->
- env_ar_params:Environ.env ->
- cumulative:bool ->
- poly:bool ->
- private_ind:bool ->
- finite:Declarations.recursivity_kind ->
- Entries.mutual_inductive_entry * UnivNames.universe_binders
+val interp_mutual_inductive_constr
+ : sigma:Evd.evar_map
+ -> template:bool option
+ -> udecl:UState.universe_decl
+ -> ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list
+ -> indnames:Names.Id.t list
+ -> arities:EConstr.t list
+ -> arityconcl:(bool * EConstr.ESorts.t) option list
+ -> constructors:(Names.Id.t list * Constr.constr list) list
+ -> env_ar_params:Environ.env
+ (** Environment with the inductives and parameters in the rel_context *)
+ -> cumulative:bool
+ -> poly:bool
+ -> private_ind:bool
+ -> finite:Declarations.recursivity_kind
+ -> Entries.mutual_inductive_entry * UnivNames.universe_binders
(************************************************************************)
(** Internal API, exported for Record *)
@@ -77,12 +75,18 @@ val should_auto_template : Id.t -> bool -> bool
automatically use template polymorphism. [x] is the name of the
inductive under consideration. *)
-val template_polymorphism_candidate :
- Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
-(** [template_polymorphism_candidate env uctx params conclsort] is
- [true] iff an inductive with params [params] and conclusion
- [conclsort] would be definable as template polymorphic. It should
- have at least one universe in its monomorphic universe context that
- can be made parametric in its conclusion sort, if one is given.
- If the [Template Check] flag is false we just check that the conclusion sort
- is not small. *)
+val template_polymorphism_candidate
+ : template_check:bool
+ -> ctor_levels:Univ.LSet.t
+ -> Entries.universes_entry
+ -> Constr.rel_context
+ -> Sorts.t option
+ -> bool
+(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params
+ conclsort] is [true] iff an inductive with params [params],
+ conclusion [conclsort] and universe levels appearing in the
+ constructor arguments [ctor_levels] would be definable as template
+ polymorphic. It should have at least one universe in its
+ monomorphic universe context that can be made parametric in its
+ conclusion sort, if one is given. If the [template_check] flag is
+ false we just check that the conclusion sort is not small. *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0e17f2b274..d48e2139d1 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -200,7 +200,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
Constrintern.Recursive full_arity impls
in
let newimpls = Id.Map.singleton recname
- (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
+ (r, l, impls @ [Some (ExplByName (Id.of_string "recproof"), Impargs.Manual, (true, false))],
scopes @ [None]) in
interp_casted_constr_evars ~program_mode:true (push_rel_context ctx env) sigma
~impls:newimpls body (lift 1 top_arity)
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 54dda09e83..c816a4eb4f 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -550,7 +550,7 @@ let intern_arg (acc, cst) (idl,(typ,ann)) =
let lib_dir = Lib.library_dp() in
let env = Global.env() in
let (mty, _, cst') = Modintern.interp_module_ast env Modintern.ModType typ in
- let () = Global.push_context_set true cst' in
+ let () = Global.push_context_set ~strict:true cst' in
let env = Global.env () in
let sobjs = get_module_sobjs false env inl mty in
let mp0 = get_module_path mty in
@@ -674,7 +674,7 @@ module RawModOps = struct
let start_module export id args res fs =
let mp = Global.start_module id in
let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let res_entry_o, subtyps, cst = match res with
| Enforce (res,ann) ->
@@ -689,7 +689,7 @@ let start_module export id args res fs =
let typs, cst = build_subtypes env mp arg_entries_r resl in
None, typs, cst
in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
openmod_info := { cur_typ = res_entry_o; cur_typs = subtyps };
let prefix = Lib.start_module export id mp fs in
Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModule prefix));
@@ -782,7 +782,7 @@ let declare_module id args res mexpr_o fs =
| None -> None
| _ -> inl_res
in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let mp_env,resolver = Global.add_module id entry inl in
(* Name consistency check : kernel vs. library *)
@@ -804,10 +804,10 @@ module RawModTypeOps = struct
let start_modtype id args mtys fs =
let mp = Global.start_modtype id in
let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
openmodtype_info := sub_mty_l;
let prefix = Lib.start_modtype id mp fs in
Nametab.(push_dir (Until 1) (prefix.obj_dir) (GlobDirRef.DirOpenModtype prefix));
@@ -835,19 +835,19 @@ let declare_modtype id args mtys (mty,ann) fs =
then we adds the module parameters to the global env. *)
let mp = Global.start_modtype id in
let arg_entries_r, cst = intern_args args in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let params = mk_params_entry arg_entries_r in
let env = Global.env () in
let mte, _, cst = Modintern.interp_module_ast env Modintern.ModType mty in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
(* We check immediately that mte is well-formed *)
let _, _, _, cst = Mod_typing.translate_mse env None inl mte in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let entry = params, mte in
let sub_mty_l, cst = build_subtypes env mp arg_entries_r mtys in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let sobjs = get_functor_sobjs false env inl entry in
let subst = map_mp (get_module_path (snd entry)) mp empty_delta_resolver in
@@ -903,7 +903,7 @@ let type_of_incl env is_mod = function
let declare_one_include (me_ast,annot) =
let env = Global.env() in
let me, kind, cst = Modintern.interp_module_ast env Modintern.ModAny me_ast in
- let () = Global.push_context_set true cst in
+ let () = Global.push_context_set ~strict:true cst in
let env = Global.env () in
let is_mod = (kind == Modintern.Module) in
let cur_mp = Lib.current_mp () in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e02f94629c..b65a126f55 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -247,7 +247,7 @@ type (_, _) entry =
| TTReference : ('self, qualid) entry
| TTBigint : ('self, string) entry
| TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry
-| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
+| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry
| TTPattern : int -> ('self, cases_pattern_expr) entry
| TTOpenBinderList : ('self, local_binder_expr list) entry
| TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry
@@ -347,12 +347,12 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym
let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with
| TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat
-| TTConstrList (typ', [], forpat) ->
- begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+| TTConstrList (s, typ', [], forpat) ->
+ begin match symbol_of_target s typ' assoc from forpat with
| MayRecNo s -> MayRecNo (Alist1 s)
| MayRecMay s -> MayRecMay (Alist1 s) end
-| TTConstrList (typ', tkl, forpat) ->
- begin match symbol_of_target InConstrEntry typ' assoc from forpat with
+| TTConstrList (s, typ', tkl, forpat) ->
+ begin match symbol_of_target s typ' assoc from forpat with
| MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl))
| MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end
| TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p))
@@ -369,7 +369,7 @@ let interp_entry forpat e = match e with
| ETProdBigint -> TTAny TTBigint
| ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat))
| ETProdPattern p -> TTAny (TTPattern p)
-| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat))
+| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat))
| ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
| ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5b97e06b2b..436648c163 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -62,17 +62,6 @@ let make_bullet s =
| '*' -> Star n
| _ -> assert false
-let parse_compat_version = let open Flags in function
- | "8.11" -> Current
- | "8.10" -> V8_10
- | "8.9" -> V8_9
- | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
- CErrors.user_err ~hdr:"get_compat_version"
- Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s ->
- CErrors.user_err ~hdr:"get_compat_version"
- Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
(* For now we just keep the top-level location of the whole
vernacular, that is to say, including attributes and control flags;
this is not very convenient for advanced clients tho, so in the
@@ -938,15 +927,7 @@ GRAMMAR EXTEND Gram
| IDENT "Remove"; IDENT "LoadPath"; dir = ne_string ->
{ VernacRemoveLoadPath dir }
- (* For compatibility *)
- | IDENT "AddPath"; dir = ne_string; "as"; alias = as_dirpath ->
- { VernacAddLoadPath (false, dir, alias) }
- | IDENT "AddRecPath"; dir = ne_string; "as"; alias = as_dirpath ->
- { VernacAddLoadPath (true, dir, alias) }
- | IDENT "DelPath"; dir = ne_string ->
- { VernacRemoveLoadPath dir }
-
- (* Type-Checking (pas dans le refman) *)
+ (* Type-Checking *)
| "Type"; c = lconstr -> { VernacGlobalCheck c }
(* Printing (careful factorization of entries) *)
@@ -1010,7 +991,7 @@ GRAMMAR EXTEND Gram
| IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." ->
{ fun g -> VernacSearch (SearchRewrite c,g, l) }
| IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." ->
- { let (sl,m) = l in fun g -> VernacSearch (SearchAbout (s::sl),g, m) }
+ { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) }
(* compatibility: SearchAbout *)
| IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." ->
{ fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) }
@@ -1199,7 +1180,7 @@ GRAMMAR EXTEND Gram
| IDENT "Notation"; id = identref;
idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
{ VernacSyntacticDefinition
- (id,(idl,c),b) }
+ (id,(idl,c),{ onlyparsing = b }) }
| IDENT "Notation"; s = lstring; ":=";
c = constr;
modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
@@ -1223,11 +1204,8 @@ GRAMMAR EXTEND Gram
] ]
;
only_parsing:
- [ [ "("; IDENT "only"; IDENT "parsing"; ")" ->
- { Some Flags.Current }
- | "("; IDENT "compat"; s = STRING; ")" ->
- { Some (parse_compat_version s) }
- | -> { None } ] ]
+ [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true }
+ | -> { false } ] ]
;
level:
[ [ IDENT "level"; n = natural -> { NumLevel n }
@@ -1243,8 +1221,6 @@ GRAMMAR EXTEND Gram
| IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
| IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
| IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
- | IDENT "compat"; s = STRING ->
- { SetCompatVersion (parse_compat_version s) }
| IDENT "format"; s1 = [s = STRING -> { CAst.make ~loc s } ];
s2 = OPT [s = STRING -> { CAst.make ~loc s } ] ->
{ begin match s1, s2 with
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2e58bf4a93..19ec0a3642 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -117,8 +117,8 @@ let display_eq ~flags env sigma t1 t2 =
let open Constrextern in
let t1 = canonize_constr sigma t1 in
let t2 = canonize_constr sigma t2 in
- let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in
- let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in
+ let ct1 = Flags.with_options flags (fun () -> extern_constr env sigma t1) () in
+ let ct2 = Flags.with_options flags (fun () -> extern_constr env sigma t2) () in
Constrexpr_ops.constr_expr_eq ct1 ct2
(** This function adds some explicit printing flags if the two arguments are
@@ -134,9 +134,9 @@ let rec pr_explicit_aux env sigma t1 t2 = function
pr_explicit_aux env sigma t1 t2 rem
else
let open Constrextern in
- let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) ()
+ let ct1 = Flags.with_options flags (fun () -> extern_constr env sigma t1) ()
in
- let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
+ let ct2 = Flags.with_options flags (fun () -> extern_constr env sigma t2) ()
in
Ppconstr.pr_lconstr_expr env sigma ct1, Ppconstr.pr_lconstr_expr env sigma ct2
@@ -697,7 +697,7 @@ let explain_cannot_find_well_typed_abstraction env sigma p l e =
str "Abstracting over the " ++
str (String.plural (List.length l) "term") ++ spc () ++
hov 0 (pr_enum (fun c -> pr_lconstr_env env sigma (EConstr.to_constr sigma c)) l) ++ spc () ++
- str "leads to a term" ++ spc () ++ pr_lconstr_goal_style_env env sigma p ++
+ str "leads to a term" ++ spc () ++ pr_ltype_env ~goal_concl_style:true env sigma p ++
spc () ++ str "which is ill-typed." ++
(match e with None -> mt () | Some e -> fnl () ++ str "Reason is: " ++ e)
@@ -1183,7 +1183,7 @@ let error_ill_formed_constructor env id c v nparams nargs =
let pr_ltype_using_barendregt_convention_env env c =
(* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
- quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c))
+ quote (pr_ltype_env ~goal_concl_style:true env (Evd.from_env env) c)
let error_bad_ind_parameters env c n v1 v2 =
let pc = pr_ltype_using_barendregt_convention_env env c in
@@ -1338,7 +1338,7 @@ let explain_reduction_tactic_error = function
| Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
let e = map_ptype_error EConstr.of_constr e in
str "The abstracted term" ++ spc () ++
- quote (pr_goal_concl_style_env env sigma c) ++
+ quote (pr_letype_env ~goal_concl_style:true env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' (Evd.from_env env') e
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b2e1a5e796..2f0b1062a7 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -210,7 +210,7 @@ let declare_one_case_analysis_scheme ind =
induction scheme, the other ones share the same code with the
appropriate type *)
if Sorts.family_leq InType kelim then
- ignore (define_individual_scheme dep UserAutomaticRequest None ind)
+ define_individual_scheme dep UserAutomaticRequest None ind
(* Induction/recursion schemes *)
@@ -248,7 +248,7 @@ let declare_one_induction_scheme ind =
else if depelim then kinds_from_type
else nondep_kinds_from_type)
in
- List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
+ List.iter (fun kind -> define_individual_scheme kind UserAutomaticRequest None ind)
elims
let declare_induction_schemes kn =
@@ -264,7 +264,7 @@ let declare_induction_schemes kn =
let declare_eq_decidability_gen internal names kn =
let mib = Global.lookup_mind kn in
if mib.mind_finite <> Declarations.CoFinite then
- ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+ define_mutual_scheme eq_dec_scheme_kind internal names kn
let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
@@ -280,14 +280,14 @@ let try_declare_eq_decidability kn =
let declare_eq_decidability = declare_eq_decidability_scheme_with []
let ignore_error f x =
- try ignore (f x) with e when CErrors.noncritical e -> ()
+ try f x with e when CErrors.noncritical e -> ()
let declare_rewriting_schemes ind =
if Hipattern.is_inductive_equality ind then begin
- ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
- ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
- ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
- UserAutomaticRequest None ind);
+ define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind;
+ define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind;
+ define_individual_scheme rew_r2l_forward_dep_scheme_kind
+ UserAutomaticRequest None ind;
(* These ones expect the equality to be symmetric; the first one also *)
(* needs eq *)
ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
@@ -310,7 +310,7 @@ let declare_congr_scheme ind =
try Coqlib.check_required_library Coqlib.logic_module_name; true
with e when CErrors.noncritical e -> false
then
- ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
+ define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind
else
warn_cannot_build_congruence ()
end
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index fd57901acd..35681aed13 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -611,7 +611,7 @@ let expand_list_rule s typ tkl x n p ll =
else if Int.equal i (p+n) then
let hds =
GramConstrListMark (p+n,true,p) :: hds
- @ [GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in
+ @ [GramConstrNonTerminal (ETProdConstrList (s, typ,tkl), Some x)] in
distribute hds ll
else
distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @
@@ -805,7 +805,6 @@ type notation_modifier = {
(* common to syn_data below *)
only_parsing : bool;
only_printing : bool;
- compat : Flags.compat_version option;
format : lstring option;
extra : (string * string) list;
}
@@ -818,7 +817,6 @@ let default = {
subtyps = [];
only_parsing = false;
only_printing = false;
- compat = None;
format = None;
extra = [];
}
@@ -877,8 +875,6 @@ let interp_modifiers modl = let open NotationMods in
interp subtyps { acc with only_parsing = true; } l
| SetOnlyPrinting :: l ->
interp subtyps { acc with only_printing = true; } l
- | SetCompatVersion v :: l ->
- interp subtyps { acc with compat = Some v; } l
| SetFormat ("text",s) :: l ->
if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
interp subtyps { acc with format = Some s; } l
@@ -916,7 +912,6 @@ let check_binder_type recvars etyps =
let not_a_syntax_modifier = function
| SetOnlyParsing -> true
| SetOnlyPrinting -> true
-| SetCompatVersion _ -> true
| _ -> false
let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
@@ -1213,32 +1208,12 @@ let check_locality_compatibility local custom i_typs =
strbrk " which is local."))
(List.uniquize allcustoms)
-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
@@ -1659,7 +1634,7 @@ let try_interp_name_alias = function
| [], { CAst.v = CRef (ref,_) } -> intern_reference ref
| _ -> raise Not_found
-let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
+let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
let vars,reversibility,pat =
try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
with Not_found ->
@@ -1673,7 +1648,6 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
List.map map vars, reversibility, pat
in
- 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)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 44e08c4819..e3e733a4b7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
(** Add a syntactic definition (as in "Notation f := ...") *)
val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
- Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
+ Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit
(** Print the Camlp5 state of a grammar *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 080629ede2..1742027076 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -161,6 +161,8 @@ open Pputils
| SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
| SearchAbout sl ->
+ keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
+ | Search sl ->
keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
let pr_option_ref_value = function
@@ -410,7 +412,6 @@ let string_of_theorem_kind = let open Decls in function
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
| SetOnlyPrinting -> keyword "only printing"
| SetOnlyParsing -> keyword "only parsing"
- | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
| SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
| SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
@@ -1057,16 +1058,12 @@ let string_of_definition_object_kind = let open Decls in function
)
| VernacHints (dbnames,h) ->
return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
- | VernacSyntacticDefinition (id,(ids,c),compat) ->
+ | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
return (
hov 2
(keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
- pr_syntax_modifiers
- (match compat with
- | None -> []
- | Some Flags.Current -> [SetOnlyParsing]
- | Some v -> [SetCompatVersion v]))
+ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
)
| VernacArguments (q, args, more_implicits, mods) ->
return (
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index ea49cae9db..eb7b28f15b 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -255,9 +255,13 @@ let needs_extra_scopes ref scopes =
let ty, _ctx = Typeops.type_of_global_in_context env ref in
aux env ty scopes
+let implicit_name_of_pos = function
+ | Constrexpr.ExplByName id -> Name id
+ | Constrexpr.ExplByPos (n,k) -> Anonymous
+
let implicit_kind_of_status = function
| None -> Anonymous, NotImplicit
- | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+ | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
let dummy = {
Vernacexpr.implicit_status = NotImplicit;
diff --git a/vernac/record.ml b/vernac/record.ml
index 49a73271f0..ea10e06d02 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -202,7 +202,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
in
let univs = Evd.check_univ_decl ~poly sigma decl in
let ubinders = Evd.universe_binders sigma in
- let ce t = Pretyping.check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr t) in
+ let ce t = Pretyping.check_evars env0 sigma (EConstr.of_constr t) in
let () = List.iter (iter_constr ce) (List.rev newps) in
ubinders, univs, template, newps, imps, ans
@@ -411,7 +411,6 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
| Polymorphic_entry (nas, ctx) ->
true, Polymorphic_entry (nas, ctx)
in
- let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance ctx) else None in
let binder_name =
match name with
| None ->
@@ -429,15 +428,32 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let type_constructor = it_mkProd_or_LetIn ind fields in
let template =
let template_candidate () =
- ComInductive.template_polymorphism_candidate (Global.env ()) univs params
+ (* we use some dummy values for the arities in the rel_context
+ as univs_of_constr doesn't care about localassums and
+ getting the real values is too annoying *)
+ let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+ let param_levels =
+ List.fold_left (fun levels d -> match d with
+ | LocalAssum _ -> levels
+ | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+ Univ.LSet.empty params
+ in
+ let ctor_levels = List.fold_left
+ (fun univs d ->
+ let univs =
+ RelDecl.fold_constr (fun c univs -> add_levels c univs) d univs
+ in
+ univs)
+ param_levels fields
+ in
+ let template_check = Environ.check_template (Global.env ()) in
+ ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params
(Some (Sorts.sort_of_univ min_univ))
in
match template with
| Some template, _ ->
(* templateness explicitly requested *)
if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
- if template && not (template_candidate ()) then
- user_err Pp.(strbrk "record cannot be made template polymorphic on any universe");
template
| None, template ->
(* auto detect template *)
@@ -461,10 +477,9 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
mind_entry_inds = blocks;
mind_entry_private = None;
mind_entry_universes = univs;
- mind_entry_variance = variance;
+ mind_entry_cumulative = poly && cumulative;
}
in
- let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let impls = List.map (fun _ -> paramimpls, []) record_data in
let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
~primitive_expected:!primitive_flag
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 535aceed15..439ec61d38 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -522,11 +522,11 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
in
start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
-let vernac_definition_hook ~poly = let open Decls in function
+let vernac_definition_hook ~local ~poly = let open Decls in function
| Coercion ->
Some (Class.add_coercion_hook ~poly)
| CanonicalStructure ->
- Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
+ Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
| SubClass ->
Some (Class.add_subclass_hook ~poly)
| _ -> None
@@ -551,7 +551,7 @@ let vernac_definition_name lid local =
let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
- let hook = vernac_definition_hook ~poly:atts.polymorphic kind in
+ let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let poly = atts.polymorphic in
let name = vernac_definition_name lid local in
@@ -560,7 +560,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
let open DefAttributes in
let scope = enforce_locality_exp atts.locality discharge in
- let hook = vernac_definition_hook ~poly:atts.polymorphic kind in
+ let hook = vernac_definition_hook ~local:atts.locality ~poly:atts.polymorphic kind in
let program_mode = atts.program in
let name = vernac_definition_name lid scope in
let red_option = match red_option with
@@ -1025,8 +1025,8 @@ let vernac_require from import qidl =
(* Coercions and canonical structures *)
-let vernac_canonical r =
- Canonical.declare_canonical_structure (smart_global r)
+let vernac_canonical ~local r =
+ Canonical.declare_canonical_structure ?local (smart_global r)
let vernac_coercion ~atts ref qids qidt =
let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
@@ -1206,10 +1206,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 ~atts lid x compat =
+let vernac_syntactic_definition ~atts lid x only_parsing =
let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
Dumpglob.dump_definition lid false "syndef";
- Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
+ Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x only_parsing
let default_env () = {
Notation_term.ninterp_var_type = Id.Map.empty;
@@ -1621,7 +1621,7 @@ let vernac_global_check c =
let c,uctx = interp_constr env sigma c in
let senv = Global.safe_env() in
let uctx = UState.context_set uctx in
- let senv = Safe_typing.push_context_set false uctx senv in
+ let senv = Safe_typing.push_context_set ~strict:false uctx senv in
let c = EConstr.to_constr sigma c in
let j = Safe_typing.typing senv c in
let env = Safe_typing.env_of_safe_env senv in
@@ -1785,6 +1785,10 @@ let () =
optread = (fun () -> !search_output_name_only);
optwrite = (:=) search_output_name_only }
+let warn_deprecated_search_about =
+ CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated"
+ (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.")
+
let vernac_search ~pstate ~atts s gopt r =
let gopt = query_command_selector gopt in
let r = interp_search_restriction r in
@@ -1815,6 +1819,10 @@ let vernac_search ~pstate ~atts s gopt r =
| SearchHead c ->
(Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search
| SearchAbout sl ->
+ warn_deprecated_search_about ();
+ (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
+ Search.prioritize_search) pr_search
+ | Search sl ->
(Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |>
Search.prioritize_search) pr_search
@@ -2085,8 +2093,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
vernac_import export qidl)
| VernacCanonical qid ->
VtDefault(fun () ->
- unsupported_attributes atts;
- vernac_canonical qid)
+ vernac_canonical ~local:(only_locality atts) qid)
| VernacCoercion (r,s,t) ->
VtDefault(fun () -> vernac_coercion ~atts r s t)
| VernacIdentityCoercion ({v=id},s,t) ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ce96d9265c..32ff8b8fb2 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -70,6 +70,7 @@ type searchable =
| SearchRewrite of constr_pattern_expr
| SearchHead of constr_pattern_expr
| SearchAbout of (bool * search_about_item) list
+ | Search of (bool * search_about_item) list
type locatable =
| LocateAny of qualid or_by_notation
@@ -104,7 +105,7 @@ type instance_flag = bool option
(* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
type export_flag = bool (* true = Export; false = Import *)
type inductive_flag = Declarations.recursivity_kind
-type onlyparsing_flag = Flags.compat_version option
+type onlyparsing_flag = { onlyparsing : bool }
(* Some v = Parse only; None = Print also.
If v<>Current, it contains the name of the coq version
which this notation is trying to be compatible with *)
@@ -184,7 +185,6 @@ type syntax_modifier =
| SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing
| SetOnlyPrinting
- | SetCompatVersion of Flags.compat_version
| SetFormat of string * lstring
type proof_end =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 13:13:33 +0000