aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/assumptions.ml2
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/comInductive.ml20
-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.mlg13
-rw-r--r--vernac/himsg.ml10
-rw-r--r--vernac/himsg.mli2
-rw-r--r--vernac/ppvernac.ml11
-rw-r--r--vernac/record.ml35
-rw-r--r--vernac/record.mli3
-rw-r--r--vernac/vernacentries.ml49
-rw-r--r--vernac/vernacexpr.ml38
14 files changed, 125 insertions, 70 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 0bcd3c64eb..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
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index e33aa38173..3bf3925b4b 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -543,7 +543,7 @@ let eqI ind l =
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
- (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed.");
+ (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
(**********************************************************************)
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index fb9d21c429..7b28895814 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -67,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
}
@@ -348,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 ~template (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)) =
@@ -424,7 +422,7 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations
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,_) ->
@@ -478,8 +476,8 @@ let interp_mutual_inductive_gen env0 ~template (uparamsl,paramsl,indl) notations
InferCumulativity.infer_inductive env_ar mind_ent
else mind_ent), Evd.universe_binders sigma, impls
-let interp_mutual_inductive ~template (paramsl,indl) notations cum poly prv finite =
- interp_mutual_inductive_gen (Global.env()) ~template ([],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 =
@@ -500,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
@@ -567,11 +565,11 @@ type uniform_inductive_flag =
| UniformParameters
| NonUniformParameters
-let do_mutual_inductive ~template 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()) ~template 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 8a2c9b8719..f23085a538 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -24,7 +24,8 @@ type uniform_inductive_flag =
| NonUniformParameters
val do_mutual_inductive :
- template:bool option -> (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+ 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
@@ -54,7 +55,6 @@ val should_auto_template : unit -> bool
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
}
@@ -69,6 +69,7 @@ val extract_mutual_inductive_declaration_components :
(** Typing mutual inductive definitions *)
val interp_mutual_inductive :
- template:bool option -> 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..7dd5471f3f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -83,11 +83,10 @@ GRAMMAR EXTEND Gram
]
;
decorated_vernac:
- [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
- | fv = vernac -> { fv } ]
- ]
+ [ [ a = LIST0 quoted_attributes ; fv = vernac ->
+ { let (f, v) = fv in (List.append (List.flatten a) f, v) } ] ]
;
- attributes:
+ quoted_attributes:
[ [ "#[" ; a = attribute_list ; "]" -> { a } ]
]
;
@@ -212,8 +211,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/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 d36586d062..724b6e62fe 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -487,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 =
@@ -627,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
@@ -636,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 ->
@@ -660,30 +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 ~template 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, auto_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
@@ -698,11 +697,11 @@ let definition_structure kind ~template 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 055a17895a..953d5ec3b6 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -26,12 +26,11 @@ val declare_projections :
(Name.t * bool) list * Constant.t option list
val definition_structure :
- inductive_kind -> template:bool option ->
+ 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 e6b3721134..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 ~template 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 ~template 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 ~template 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 ~template 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
@@ -613,7 +627,7 @@ let vernac_inductive ~atts cum lo finite indl =
let (coe, (lid, ce)) = l in
let coe' = if coe then Some true else None in
let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in
- vernac_record ~template 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
@@ -636,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 ~template 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
@@ -662,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 ~template 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")
(*
@@ -1950,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 *)
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 00:34:47 +0000