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/classes.ml2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/comInductive.ml44
-rw-r--r--vernac/comInductive.mli40
-rw-r--r--vernac/comProgramFixpoint.ml2
-rw-r--r--vernac/declaremods.ml22
-rw-r--r--vernac/himsg.ml14
-rw-r--r--vernac/indschemes.ml18
-rw-r--r--vernac/prettyp.ml6
-rw-r--r--vernac/record.ml9
-rw-r--r--vernac/vernacentries.ml2
12 files changed, 80 insertions, 85 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/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 a001420f74..8a403e5a03 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -255,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 2aee9bd47f..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,18 +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 ~ctor_levels 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 ~ctor_levels uctx params conclu
in
- not (template_check && Univ.LSet.is_empty conclunivs)
+ not (Univ.LSet.is_empty conclunivs)
| Entries.Polymorphic_entry _ -> false
let check_param = function
@@ -350,33 +350,28 @@ 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 ||
let ctor_levels =
@@ -390,7 +385,7 @@ let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_pa
List.fold_left (fun levels c -> add_levels c levels)
param_levels ctypes
in
- template_polymorphism_candidate env0 ~ctor_levels uctx ctx_params concl
+ 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 ->
@@ -408,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;
@@ -417,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
@@ -492,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
@@ -505,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 ef05b213d8..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 *)
@@ -78,17 +76,17 @@ val should_auto_template : Id.t -> bool -> bool
inductive under consideration. *)
val template_polymorphism_candidate
- : Environ.env
+ : template_check:bool
-> ctor_levels:Univ.LSet.t
-> Entries.universes_entry
-> Constr.rel_context
-> Sorts.t option
-> bool
-(** [template_polymorphism_candidate env ~ctor_levels uctx params
+(** [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
+ 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/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/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 d85b71df44..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 ->
@@ -447,7 +446,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
univs)
param_levels fields
in
- ComInductive.template_polymorphism_candidate (Global.env ()) ~ctor_levels univs params
+ 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
@@ -477,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 e4965614d8..439ec61d38 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:51:38 +0000