aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml36
-rw-r--r--vernac/assumptions.mli5
-rw-r--r--vernac/comInductive.ml84
-rw-r--r--vernac/comInductive.mli7
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/g_proofs.mlg1
-rw-r--r--vernac/g_vernac.mlg6
-rw-r--r--vernac/himsg.ml10
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/obligations.ml6
-rw-r--r--vernac/ppvernac.ml11
-rw-r--r--vernac/record.ml57
-rw-r--r--vernac/record.mli4
-rw-r--r--vernac/vernacentries.ml58
-rw-r--r--vernac/vernacexpr.ml38
-rw-r--r--vernac/vernacinterp.ml5
-rw-r--r--vernac/vernacinterp.mli4
17 files changed, 221 insertions, 115 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index e5d2382e46..b000745961 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -71,7 +71,7 @@ let rec fields_of_functor f subs mp0 args = function
let rec lookup_module_in_impl mp =
match mp with
| MPfile _ -> Global.lookup_module mp
- | MPbound _ -> assert false
+ | MPbound _ -> Global.lookup_module mp
| MPdot (mp',lab') ->
if ModPath.equal mp' (Global.current_modpath ()) then
Global.lookup_module mp
@@ -213,25 +213,25 @@ let rec traverse current ctx accu t = match Constr.kind t with
and traverse_object ?inhabits (curr, data, ax2ty) body obj =
let data, ax2ty =
- let already_in = Refmap_env.mem obj data in
+ let already_in = GlobRef.Map_env.mem obj data in
match body () with
| None ->
let data =
- if not already_in then Refmap_env.add obj Refset_env.empty data else data in
+ if not already_in then GlobRef.Map_env.add obj GlobRef.Set_env.empty data else data in
let ax2ty =
if Option.is_empty inhabits then ax2ty else
let ty = Option.get inhabits in
- try let l = Refmap_env.find obj ax2ty in Refmap_env.add obj (ty::l) ax2ty
- with Not_found -> Refmap_env.add obj [ty] ax2ty in
+ try let l = GlobRef.Map_env.find obj ax2ty in GlobRef.Map_env.add obj (ty::l) ax2ty
+ with Not_found -> GlobRef.Map_env.add obj [ty] ax2ty in
data, ax2ty
| Some body ->
if already_in then data, ax2ty else
let contents,data,ax2ty =
traverse (label_of obj) Context.Rel.empty
- (Refset_env.empty,data,ax2ty) body in
- Refmap_env.add obj contents data, ax2ty
+ (GlobRef.Set_env.empty,data,ax2ty) body in
+ GlobRef.Map_env.add obj contents data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects the references occurring in the declaration of mutual inductive
definitions. All the constructors and names of a mutual inductive
@@ -244,14 +244,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Invariant : I_0 \in data iff I_i \in data iff c_ij \in data
where I_0, I_1, ... are in the same mutual definition and c_ij
are all their constructors. *)
- if Refmap_env.mem firstind_ref data then data, ax2ty else
+ if GlobRef.Map_env.mem firstind_ref data then data, ax2ty else
let mib = lookup_mind mind in
(* Collects references of parameters *)
let param_ctx = mib.mind_params_ctxt in
let nparam = List.length param_ctx in
let accu =
traverse_context label Context.Rel.empty
- (Refset_env.empty, data, ax2ty) param_ctx
+ (GlobRef.Set_env.empty, data, ax2ty) param_ctx
in
(* Build the context of all arities *)
let arities_ctx =
@@ -283,14 +283,14 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
(* Maps all these dependencies to inductives and constructors*)
let data = Array.fold_left_i (fun n data oib ->
let ind = (mind, n) in
- let data = Refmap_env.add (IndRef ind) contents data in
+ let data = GlobRef.Map_env.add (IndRef ind) contents data in
Array.fold_left_i (fun k data _ ->
- Refmap_env.add (ConstructRef (ind, k+1)) contents data
+ GlobRef.Map_env.add (ConstructRef (ind, k+1)) contents data
) data oib.mind_consnames) data mib.mind_packets
in
data, ax2ty
in
- (Refset_env.add obj curr, data, ax2ty)
+ (GlobRef.Set_env.add obj curr, data, ax2ty)
(** Collects references in a rel_context. *)
and traverse_context current ctx accu ctxt =
@@ -307,7 +307,7 @@ and traverse_context current ctx accu ctxt =
let traverse current t =
let () = modcache := MPmap.empty in
- traverse current Context.Rel.empty (Refset_env.empty, Refmap_env.empty, Refmap_env.empty) t
+ traverse current Context.Rel.empty (GlobRef.Set_env.empty, GlobRef.Map_env.empty, GlobRef.Map_env.empty) t
(** Hopefully bullet-proof function to recover the type of a constant. It just
ignores all the universe stuff. There are many issues that can arise when
@@ -330,12 +330,12 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
let accu =
if cb.const_typing_flags.check_guarded then accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Guarded kn, l)) Constr.mkProp accu
in
if not (Declareops.constant_has_body cb) || not cb.const_typing_flags.check_universes then
let t = type_of_constant cb in
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Constant kn,l)) t accu
else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
let t = type_of_constant cb in
@@ -350,7 +350,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
if mind.mind_typing_flags.check_guarded then
accu
else
- let l = try Refmap_env.find obj ax2ty with Not_found -> [] in
+ let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
ContextObjectMap.add (Axiom (Positive m, l)) Constr.mkProp accu
in
- Refmap_env.fold fold graph ContextObjectMap.empty
+ GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 751e79d89c..aead345d8c 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -10,7 +10,6 @@
open Names
open Constr
-open Globnames
open Printer
(** Collects all the objects on which a term directly relies, bypassing kernel
@@ -22,8 +21,8 @@ open Printer
*)
val traverse :
Label.t -> constr ->
- (Refset_env.t * Refset_env.t Refmap_env.t *
- (Label.t * Constr.rel_context * types) list Refmap_env.t)
+ (GlobRef.Set_env.t * GlobRef.Set_env.t GlobRef.Map_env.t *
+ (Label.t * Constr.rel_context * types) list GlobRef.Map_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 716c40dbff..7b28895814 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -35,6 +35,18 @@ module RelDecl = Context.Rel.Declaration
(* 3b| Mutual inductive definitions *)
+let should_auto_template =
+ let open Goptions in
+ let auto = ref true in
+ let _ = declare_bool_option
+ { optdepr = false;
+ optname = "Automatically make some inductive types template polymorphic";
+ optkey = ["Auto";"Template";"Polymorphism"];
+ optread = (fun () -> !auto);
+ optwrite = (fun b -> auto := b); }
+ in
+ fun () -> !auto
+
let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function
| CProdN (bl,c) -> CProdN (bl,complete_conclusion a cs c)
| CLetIn (na,b,t,c) -> CLetIn (na,b,t,complete_conclusion a cs c)
@@ -55,7 +67,6 @@ let push_types env idl tl =
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -113,17 +124,16 @@ let rec check_anonymous_type ind =
| GCast (e, _) -> check_anonymous_type e
| _ -> false
-let make_conclusion_flexible sigma ty poly =
- if poly && Term.isArity ty then
- let _, concl = Term.destArity ty in
- match concl with
- | Type u ->
- (match Univ.universe_level u with
+let make_conclusion_flexible sigma = function
+ | None -> sigma
+ | Some s ->
+ (match EConstr.ESorts.kind sigma s with
+ | Type u ->
+ (match Univ.universe_level u with
| Some u ->
Evd.make_flexible_variable sigma ~algebraic:true u
| None -> sigma)
- | _ -> sigma
- else sigma
+ | _ -> sigma)
let is_impredicative env u =
u = Prop || (is_impredicative_set env && u = Set)
@@ -133,10 +143,12 @@ let interp_ind_arity env sigma ind =
let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
let pseudo_poly = check_anonymous_type c in
- let () = if not (Reductionops.is_arity env sigma t) then
+ match Reductionops.sort_of_arity env sigma t with
+ | exception Invalid_argument _ ->
user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
- in
- sigma, (t, pseudo_poly, impls)
+ | s ->
+ let concl = if pseudo_poly then Some s else None in
+ sigma, (t, concl, impls)
let interp_cstrs env sigma impls mldata arity ind =
let cnames,ctyps = List.split ind.ind_lc in
@@ -335,13 +347,12 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
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_gen env0 (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite =
check_all_names_different indl;
List.iter check_param paramsl;
if not (List.is_empty uparamsl) && not (List.is_empty notations)
then user_err (str "Inductives with uniform parameters may not have attached notations.");
- let pl = (List.hd indl).ind_univs in
- let sigma, decl = interp_univ_decl_opt env0 pl in
+ let sigma, udecl = interp_univ_decl_opt env0 udecl in
let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
interp_context_evars env0 sigma uparamsl in
let sigma, (impls, ((env_params, ctx_params), userimpls)) =
@@ -363,7 +374,7 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
(* Compute interpretation metadatas *)
let indimpls = List.map (fun (_, _, impls) -> userimpls @
lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
- let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
+ let arities = List.map pi1 arities and arityconcl = List.map pi2 arities 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,15 +413,16 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
let nf = Evarutil.nf_evars_universes sigma in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let arities = List.map EConstr.(to_constr sigma) arities in
- let sigma = List.fold_left2 (fun sigma ty poly -> make_conclusion_flexible sigma ty poly) sigma arities aritypoly in
+ let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
let sigma = Evd.minimize_universes sigma in
let nf = Evarutil.nf_evars_universes sigma in
let arities = List.map nf arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
+ let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
- let uctx = Evd.check_univ_decl ~poly sigma decl 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 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,_) ->
@@ -418,13 +430,23 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
constructors;
(* Build the inductive entries *)
- let entries = List.map4 (fun ind arity template (cnames,ctypes,cimpls) -> {
- mind_entry_typename = ind.ind_name;
- mind_entry_arity = arity;
- mind_entry_template = template;
- mind_entry_consnames = cnames;
- mind_entry_lc = ctypes
- }) indl arities aritypoly constructors in
+ let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+ let template = match template with
+ | Some template ->
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None ->
+ should_auto_template () && not poly &&
+ Option.cata (fun s -> not (Sorts.is_small s)) false concl
+ in
+ { mind_entry_typename = ind.ind_name;
+ mind_entry_arity = arity;
+ mind_entry_template = template;
+ mind_entry_consnames = cnames;
+ mind_entry_lc = ctypes
+ })
+ indl arities arityconcl constructors
+ in
let impls =
let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
@@ -454,8 +476,8 @@ let interp_mutual_inductive_gen env0 (uparamsl,paramsl,indl) notations cum poly
InferCumulativity.infer_inductive env_ar mind_ent
else mind_ent), Evd.universe_binders sigma, impls
-let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
- interp_mutual_inductive_gen (Global.env()) ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite =
+ interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite
(* Very syntactical equality *)
let eq_local_binders bl1 bl2 =
@@ -476,8 +498,8 @@ let extract_params indl =
params
let extract_inductive indl =
- List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> {
- ind_name = indname; ind_univs = pl;
+ List.map (fun ({CAst.v=indname},_,ar,lc) -> {
+ ind_name = indname;
ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar;
ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
}) indl
@@ -543,11 +565,11 @@ type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
-let do_mutual_inductive indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite =
let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
(* Interpret the types *)
let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
- let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) indl ntns cum poly prv finite in
+ let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in
(* Declare the mutual inductive block with its associated schemes *)
ignore (declare_mutual_inductive_with_eliminations mie pl impls);
(* Declare the possible notations of inductive types *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 4e30ed7de5..f23085a538 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,6 +24,7 @@ type uniform_inductive_flag =
| NonUniformParameters
val do_mutual_inductive :
+ template:bool option -> universe_decl_expr option ->
(one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
Declarations.recursivity_kind -> unit
@@ -45,6 +46,8 @@ val declare_mutual_inductive_with_eliminations :
mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
MutInd.t
+val should_auto_template : unit -> bool
+
(** Exported for Funind *)
(** Extracting the semantical components out of the raw syntax of mutual
@@ -52,7 +55,6 @@ val declare_mutual_inductive_with_eliminations :
type structured_one_inductive_expr = {
ind_name : Id.t;
- ind_univs : universe_decl_expr option;
ind_arity : constr_expr;
ind_lc : (Id.t * constr_expr) list
}
@@ -67,6 +69,7 @@ val extract_mutual_inductive_declaration_components :
(** Typing mutual inductive definitions *)
val interp_mutual_inductive :
- structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+ template:bool option -> universe_decl_expr option -> structured_inductive_expr ->
+ decl_notation list -> cumulative_inductive_flag ->
polymorphic -> private_flag -> Declarations.recursivity_kind ->
mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 504e7095b0..7cf4e64805 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,6 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
| PretypeError(ctx,sigma,te) ->
wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+ | Notation.NumeralNotationError(ctx,sigma,te) ->
+ wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te)
| Typeclasses_errors.TypeClassError(env, te) ->
wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
| Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index dacef6e211..ecc7d3ff88 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -13,6 +13,7 @@
open Glob_term
open Constrexpr
open Vernacexpr
+open Hints
open Proof_global
open Pcoq
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 44c0159d1b..650b28ea67 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,8 +212,10 @@ GRAMMAR EXTEND Gram
| IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
- | IDENT "Register"; IDENT "Inline"; id = identref ->
- { VernacRegister(id, RegisterInline) }
+ | IDENT "Register"; g = global; "as"; quid = qualid ->
+ { VernacRegister(g, RegisterRetroknowledge quid) }
+ | IDENT "Register"; IDENT "Inline"; g = global ->
+ { VernacRegister(g, RegisterInline) }
| IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
| IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a4650cfd92..e7b2a0e8a6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1315,3 +1315,13 @@ let explain_reduction_tactic_error = function
quote (pr_goal_concl_style_env env sigma c) ++
spc () ++ str "is not well typed." ++ fnl () ++
explain_type_error env' (Evd.from_env env') e
+
+let explain_numeral_notation_error env sigma = function
+ | Notation.UnexpectedTerm c ->
+ (strbrk "Unexpected term " ++
+ pr_constr_env env sigma c ++
+ strbrk " while parsing a numeral notation.")
+ | Notation.UnexpectedNonOptionTerm c ->
+ (strbrk "Unexpected non-option term " ++
+ pr_constr_env env sigma c ++
+ strbrk " while parsing a numeral notation.")
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 91caddcf13..02b3c45501 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -46,3 +46,5 @@ val explain_module_internalization_error :
val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
+
+val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 14d7642328..3987e53bc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -523,11 +523,11 @@ let declare_mutual_definition l =
(List.map (fun x ->
let subs, typ = (subst_body true x) in
let env = Global.env () in
- let sigma = Evd.from_env env in
+ let sigma = Evd.from_ctx x.prg_ctx in
let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
- let term = EConstr.Unsafe.to_constr term in
- let typ = EConstr.Unsafe.to_constr typ in
+ let term = EConstr.to_constr sigma term in
+ let typ = EConstr.to_constr sigma typ in
x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
in
(* let fixdefs = List.map reduce_fix fixdefs in *)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 63e9e4fe49..b4b3aead91 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -178,11 +178,11 @@ open Pputils
| [] -> mt()
| _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
- let pr_reference_or_constr pr_c = function
+ let pr_reference_or_constr pr_c = let open Hints in function
| HintsReference r -> pr_qualid r
| HintsConstr c -> pr_c c
- let pr_hint_mode = function
+ let pr_hint_mode = let open Hints in function
| ModeInput -> str"+"
| ModeNoHeadEvar -> str"!"
| ModeOutput -> str"-"
@@ -194,6 +194,7 @@ open Pputils
let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
+ let open Hints in
match h with
| HintsResolve l ->
keyword "Resolve " ++ prlist_with_sep sep
@@ -1161,7 +1162,11 @@ open Pputils
| VernacRegister (id, RegisterInline) ->
return (
hov 2
- (keyword "Register Inline" ++ spc() ++ pr_lident id)
+ (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+ )
+ | VernacRegister (id, RegisterRetroknowledge n) ->
+ return (
+ hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n)
)
| VernacComments l ->
return (
diff --git a/vernac/record.ml b/vernac/record.ml
index 6b5c538df2..724b6e62fe 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -393,14 +393,14 @@ open Typeclasses
let declare_structure finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
let nparams = List.length params in
- let template, ctx =
+ let poly, ctx =
match univs with
| Monomorphic_ind_entry ctx ->
- template, Monomorphic_const_entry Univ.ContextSet.empty
+ false, Monomorphic_const_entry Univ.ContextSet.empty
| Polymorphic_ind_entry ctx ->
- false, Polymorphic_const_entry ctx
+ true, Polymorphic_const_entry ctx
| Cumulative_ind_entry cumi ->
- false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+ true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -417,6 +417,18 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
+ let template =
+ match template with
+ | Some template, _ ->
+ (* templateness explicitly requested *)
+ if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+ template
+ | None, template ->
+ (* auto detect template *)
+ ComInductive.should_auto_template () && template && not poly &&
+ let _, s = Reduction.dest_arity (Global.env()) arity in
+ not (Sorts.is_small s)
+ in
{ mind_entry_typename = id;
mind_entry_arity = arity;
mind_entry_template = template;
@@ -441,7 +453,6 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let cstr = (rsp, 1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
let build = ConstructRef cstr in
- let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
rsp
@@ -476,10 +487,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
let cst = Declare.declare_constant id
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let cstu = (cst, match univs with
- | Polymorphic_const_entry univs -> Univ.UContext.instance univs
- | Monomorphic_const_entry _ -> Univ.Instance.empty)
+ let inst, univs = match univs with
+ | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+ | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
in
+ let cstu = (cst, inst) in
let inst_type = appvectc (mkConstU cstu)
(Termops.rel_vect 0 (List.length params)) in
let proj_type =
@@ -616,7 +628,7 @@ let check_unique_names records =
| Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc
| _ -> acc in
let allnames =
- List.fold_left (fun acc (_, id, _, _, cfs, _, _) ->
+ List.fold_left (fun acc (_, id, _, cfs, _, _) ->
id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
in
match List.duplicates Id.equal allnames with
@@ -625,19 +637,19 @@ let check_unique_names records =
let check_priorities kind records =
let isnot_class = match kind with Class false -> false | _ -> true in
- let has_priority (_, _, _, _, cfs, _, _) =
+ let has_priority (_, _, _, cfs, _, _) =
List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs
in
if isnot_class && List.exists has_priority records then
user_err Pp.(str "Priorities only allowed for type class substructures")
let extract_record_data records =
- let map (is_coe, id, _, _, cfs, idbuild, s) =
+ let map (is_coe, id, _, cfs, idbuild, s) =
let fs = List.map (fun (((_, f), _), _) -> f) cfs in
id.CAst.v, s, List.map snd cfs, fs
in
let data = List.map map records in
- let pss = List.map (fun (_, _, _, ps, _, _, _) -> ps) records in
+ let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
let ps = match pss with
| [] -> CErrors.anomaly (str "Empty record block")
| ps :: rem ->
@@ -649,29 +661,28 @@ let extract_record_data records =
in
ps
in
- (** FIXME: Same issue as #7754 *)
- let _, _, pl, _, _, _, _ = List.hd records in
- pl, ps, data
+ ps, data
(* [fs] corresponds to fields and [ps] to parameters; [coers] is a
list telling if the corresponding fields must me declared as coercions
or subinstances. *)
-let definition_structure kind cum poly finite records =
+let definition_structure udecl kind ~template cum poly finite records =
let () = check_unique_names records in
let () = check_priorities kind records in
- let pl, ps, data = extract_record_data records in
- let pl, univs, template, params, implpars, data =
+ let ps, data = extract_record_data records in
+ let ubinders, univs, auto_template, params, implpars, data =
States.with_state_protection (fun () ->
- typecheck_params_and_fields finite (kind = Class true) poly pl ps data) () in
+ typecheck_params_and_fields finite (kind = Class true) poly udecl ps data) () in
+ let template = template, auto_template in
match kind with
| Class def ->
- let (_, id, _, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
+ let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
| [r], [d] -> r, d
| _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
in
let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
- declare_class finite def cum pl univs id.CAst.v idbuild
+ declare_class finite 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
@@ -686,11 +697,11 @@ let definition_structure kind cum poly finite records =
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
- let map (arity, implfs, fields) (is_coe, id, _, _, cfs, idbuild, _) =
+ let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in
id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
in
let data = List.map2 map data records in
- let inds = declare_structure finite pl univs implpars params template data in
+ let inds = declare_structure finite ubinders univs implpars params template data in
List.map (fun ind -> IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 567f2b3138..953d5ec3b6 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,11 +26,11 @@ val declare_projections :
(Name.t * bool) list * Constant.t option list
val definition_structure :
- inductive_kind -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
+ universe_decl_expr option -> inductive_kind -> template:bool option ->
+ Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
Declarations.recursivity_kind ->
(coercion_flag *
Names.lident *
- universe_decl_expr option *
local_binder_expr list *
(local_decl_expr with_instance with_priority with_notation) list *
Id.t * constr_expr option) list ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 681dce3ca3..015d5fabef 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -555,9 +555,9 @@ let should_treat_as_uniform () =
then ComInductive.UniformParameters
else ComInductive.NonUniformParameters
-let vernac_record cum k poly finite records =
+let vernac_record ~template udecl cum k poly finite records =
let is_cumulative = should_treat_as_cumulative cum poly in
- let map ((coe, (id, pl)), binders, sort, nameopt, cfs) =
+ let map ((coe, id), binders, sort, nameopt, cfs) =
let const = match nameopt with
| None -> add_prefix "Build_" id.v
| Some lid ->
@@ -574,10 +574,22 @@ let vernac_record cum k poly finite records =
in
List.iter iter cfs
in
- coe, id, pl, binders, cfs, const, sort
+ coe, id, binders, cfs, const, sort
in
let records = List.map map records in
- ignore(Record.definition_structure k is_cumulative poly finite records)
+ ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records)
+
+let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
+ match indl with
+ | [] -> assert false
+ | (((coe,(id,udecl)),b,c,k,d),e) :: rest ->
+ let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) ->
+ if Option.has_some udecl
+ then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.")
+ else (((coe,id),b,c,k,d),e))
+ rest
+ in
+ udecl, (((coe,id),b,c,k,d),e) :: rest
(** When [poly] is true the type is declared polymorphic. When [lo] is true,
then the type is declared private (as per the [Private] keyword). [finite]
@@ -585,8 +597,9 @@ let vernac_record cum k poly finite records =
neither. *)
let vernac_inductive ~atts cum lo finite indl =
let open Pp in
+ let udecl, indl = extract_inductive_udecl indl in
if Dumpglob.dump () then
- List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) ->
+ List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
match cstrs with
| Constructors cstrs ->
Dumpglob.dump_definition lid false "ind";
@@ -594,6 +607,7 @@ let vernac_inductive ~atts cum lo finite indl =
Dumpglob.dump_definition lid false "constr") cstrs
| _ -> () (* dumping is done by vernac_record (called below) *) )
indl;
+
let is_record = function
| ((_ , _ , _ , _, RecordDecl _), _) -> true
| _ -> false
@@ -606,13 +620,14 @@ let vernac_inductive ~atts cum lo finite indl =
| [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
| _ -> None
in
+ let template = atts.template in
if Option.has_some is_defclass then
(** Definitional class case *)
let (id, bl, c, l) = Option.get is_defclass in
let (coe, (lid, ce)) = l in
let coe' = if coe then Some true else None in
let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
- vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
+ vernac_record ~template udecl cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
else if List.for_all is_record indl then
(** Mutual record case *)
let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -635,7 +650,7 @@ let vernac_inductive ~atts cum lo finite indl =
let ((_, _, _, kind, _), _) = List.hd indl in
let kind = match kind with Class _ -> Class false | _ -> kind in
let recordl = List.map unpack indl in
- vernac_record cum kind atts.polymorphic finite recordl
+ vernac_record ~template udecl cum kind atts.polymorphic finite recordl
else if List.for_all is_constructor indl then
(** Mutual inductive case *)
let check_kind ((_, _, _, kind, _), _) = match kind with
@@ -661,7 +676,7 @@ let vernac_inductive ~atts cum lo finite indl =
let indl = List.map unpack indl in
let is_cumulative = should_treat_as_cumulative cum atts.polymorphic in
let uniform = should_treat_as_uniform () in
- ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo ~uniform finite
+ ComInductive.do_mutual_inductive ~template udecl indl is_cumulative atts.polymorphic lo ~uniform finite
else
user_err (str "Mixed record-inductive definitions are not allowed")
(*
@@ -1949,14 +1964,23 @@ let vernac_locate = function
| LocateOther (s, qid) -> print_located_other s qid
| LocateFile f -> locate_file f
-let vernac_register id r =
+let vernac_register qid r =
+ let gr = Smartlocate.global_with_alias qid in
if Proof_global.there_are_pending_proofs () then
user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
- let kn = Constrintern.global_reference id.v in
- if not (isConstRef kn) then
- user_err Pp.(str "Register inline: a constant is expected");
match r with
- | RegisterInline -> Global.register_inline (destConstRef kn)
+ | RegisterInline ->
+ if not (isConstRef gr) then
+ user_err Pp.(str "Register inline: a constant is expected");
+ Global.register_inline (destConstRef gr)
+ | RegisterRetroknowledge n ->
+ let path, id = Libnames.repr_qualid n in
+ if DirPath.equal path Retroknowledge.int31_path
+ then
+ let f = Retroknowledge.(KInt31 (int31_field_of_string (Id.to_string id))) in
+ Global.register f gr
+ else
+ user_err Pp.(str "Register in unknown namespace: " ++ str (DirPath.to_string path))
(********************)
(* Proof management *)
@@ -2358,6 +2382,14 @@ let attributes_of_flags f atts =
(Some false, atts)
| ("polymorphic" | "monomorphic") ->
user_err Pp.(str "Polymorphism specified twice")
+ | "template" when atts.template = None ->
+ assert_empty k v;
+ polymorphism, { atts with template = Some true }
+ | "notemplate" when atts.template = None ->
+ assert_empty k v;
+ polymorphism, { atts with template = Some false }
+ | "template" | "notemplate" ->
+ user_err Pp.(str "Templateness specified twice")
| "local" when Option.is_empty atts.locality ->
assert_empty k v;
(polymorphism, { atts with locality = Some true })
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 11b2a7d802..13c8830b84 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -16,11 +16,11 @@ open Libnames
type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
type goal_selector = Goal_select.t =
- | SelectAlreadyFocused
- | SelectNth of int
- | SelectList of (int * int) list
- | SelectId of Id.t
- | SelectAll
+ | SelectAlreadyFocused [@ocaml.deprecated "Use Goal_select.SelectAlreadyFocused"]
+ | SelectNth of int [@ocaml.deprecated "Use Goal_select.SelectNth"]
+ | SelectList of (int * int) list [@ocaml.deprecated "Use Goal_select.SelectList"]
+ | SelectId of Id.t [@ocaml.deprecated "Use Goal_select.SelectId"]
+ | SelectAll [@ocaml.deprecated "Use Goal_select.SelectAll"]
[@@ocaml.deprecated "Use Goal_select.t"]
type goal_identifier = string
@@ -103,14 +103,14 @@ type comment =
| CommentInt of int
type reference_or_constr = Hints.reference_or_constr =
- | HintsReference of qualid
- | HintsConstr of constr_expr
+ | HintsReference of qualid [@ocaml.deprecated "Use Hints.HintsReference"]
+ | HintsConstr of constr_expr [@ocaml.deprecated "Use Hints.HintsConstr"]
[@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
type hint_mode = Hints.hint_mode =
- | ModeInput (* No evars *)
- | ModeNoHeadEvar (* No evar at the head *)
- | ModeOutput (* Anything *)
+ | ModeInput [@ocaml.deprecated "Use Hints.ModeInput"]
+ | ModeNoHeadEvar [@ocaml.deprecated "Use Hints.ModeNoHeadEvar"]
+ | ModeOutput [@ocaml.deprecated "Use Hints.ModeOutput"]
[@@ocaml.deprecated "Please use [Hints.hint_mode]"]
type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
@@ -128,13 +128,21 @@ type 'a hints_transparency_target = 'a Hints.hints_transparency_target =
type hints_expr = Hints.hints_expr =
| HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsResolveIFF of bool * qualid list * int option
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsImmediate of Hints.reference_or_constr list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsUnfold of qualid list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsTransparency of qualid hints_transparency_target * bool
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsMode of qualid * Hints.hint_mode list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsConstructors of qualid list
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
| HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
+ [@ocaml.deprecated "Use the constructor in module [Hints]"]
[@@ocaml.deprecated "Please use [Hints.hints_expr]"]
type search_restriction =
@@ -202,7 +210,7 @@ type inductive_expr =
constructor_list_or_record_decl_expr
type one_inductive_expr =
- ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
+ lident * local_binder_expr list * constr_expr option * constructor_expr list
type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
and typeclass_context = typeclass_constraint list
@@ -278,6 +286,7 @@ type extend_name =
It will be extended with primitive inductive types and operators *)
type register_kind =
| RegisterInline
+ | RegisterRetroknowledge of qualid
type bullet = Proof_bullet.t
[@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
@@ -288,7 +297,9 @@ type bullet = Proof_bullet.t
type 'a module_signature = 'a Declaremods.module_signature =
| Enforce of 'a (** ... : T *)
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
| Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
[@@ocaml.deprecated "please use [Declaremods.module_signature]."]
(** Which module inline annotations should we honor,
@@ -297,8 +308,11 @@ type 'a module_signature = 'a Declaremods.module_signature =
type inline = Declaremods.inline =
| NoInline
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
| DefaultInline
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
| InlineAt of int
+ [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
[@@ocaml.deprecated "please use [Declaremods.inline]."]
type module_ast_inl = module_ast * Declaremods.inline
@@ -438,7 +452,7 @@ type nonrec vernac_expr =
| VernacPrint of printable
| VernacSearch of searchable * Goal_select.t option * search_restriction
| VernacLocate of locatable
- | VernacRegister of lident * register_kind
+ | VernacRegister of qualid * register_kind
| VernacComments of comment list
(* Proof management *)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 1bb1414f3d..2746cbd144 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -21,12 +21,13 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ template : bool option;
program : bool;
deprecated : deprecation option;
}
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
- { loc ; locality ; polymorphic ; program ; deprecated }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
+ { loc ; locality ; polymorphic ; program ; deprecated; template }
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 46468b3098..62a178b555 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -18,12 +18,14 @@ type atts = {
loc : Loc.t option;
locality : bool option;
polymorphic : bool;
+ template : bool option;
program : bool;
deprecated : deprecation option;
}
val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
- ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
+ ?polymorphic: bool -> ?template:bool option ->
+ ?program: bool -> ?deprecated: deprecation option -> unit -> atts
type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 11:15:16 +0000