aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml72
-rw-r--r--vernac/class.mli4
-rw-r--r--vernac/classes.ml6
-rw-r--r--vernac/comDefinition.ml6
-rw-r--r--vernac/comDefinition.mli2
-rw-r--r--vernac/comFixpoint.ml10
-rw-r--r--vernac/comProgramFixpoint.ml35
-rw-r--r--vernac/declareDef.ml36
-rw-r--r--vernac/declareDef.mli2
-rw-r--r--vernac/egramml.ml4
-rw-r--r--vernac/egramml.mli2
-rw-r--r--vernac/g_vernac.mlg6
-rw-r--r--vernac/indschemes.ml8
-rw-r--r--vernac/lemmas.ml49
-rw-r--r--vernac/lemmas.mli35
-rw-r--r--vernac/obligations.ml28
-rw-r--r--vernac/obligations.mli8
-rw-r--r--vernac/ppvernac.ml12
-rw-r--r--vernac/search.ml6
-rw-r--r--vernac/vernacentries.ml61
-rw-r--r--vernac/vernacentries.mli19
-rw-r--r--vernac/vernacexpr.ml3
22 files changed, 207 insertions, 207 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index dee7541d37..148d4437fa 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -62,29 +62,23 @@ exception NoDecidabilityCoInductive
exception ConstructorWithNonParametricInductiveType of inductive
exception DecidabilityIndicesNotSupported
-let constr_of_global g = lazy (UnivGen.constr_of_global g)
-
(* Some pre declaration of constant we are going to use *)
-let bb = constr_of_global Coqlib.glob_bool
-
-let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop
+let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb_prop")
let andb_true_intro = fun _ ->
UnivGen.constr_of_global
- (Coqlib.build_bool_type()).Coqlib.andb_true_intro
-
-let tt = constr_of_global Coqlib.glob_true
-
-let ff = constr_of_global Coqlib.glob_false
-
-let eq = constr_of_global Coqlib.glob_eq
-
-let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ())
+ (Coqlib.lib_ref "core.bool.andb_true_intro")
-let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb
+(* We avoid to use lazy as the binding of constants can change *)
+let bb () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.type")
+let tt () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.true")
+let ff () = UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.false")
+let eq () = UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")
-let induct_on c = induction false None c None None
+let sumbool () = UnivGen.constr_of_global (Coqlib.lib_ref "core.sumbool.type")
+let andb = fun _ -> UnivGen.constr_of_global (Coqlib.lib_ref "core.bool.andb")
+let induct_on c = induction false None c None None
let destruct_on c = destruct false None c None None
let destruct_on_using c id =
@@ -119,7 +113,7 @@ let mkFullInd (ind,u) n =
else mkIndU (ind,u)
let check_bool_is_defined () =
- try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in ()
+ try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
let check_no_indices mib =
@@ -160,7 +154,7 @@ let build_beq_scheme mode kn =
let eqs_typ = List.map (fun aa ->
let a = lift !lift_cnt aa in
incr lift_cnt;
- myArrow a (myArrow a (Lazy.force bb))
+ myArrow a (myArrow a (bb ()))
) ext_rel_list in
let eq_input = List.fold_left2
@@ -259,7 +253,7 @@ let build_beq_scheme mode kn =
List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
(mkLambda (Anonymous,
mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
- (Lazy.force bb)))
+ (bb ())))
(List.rev rettyp_l) in
(* make_one_eq *)
(* do the [| C1 ... => match Y with ... end
@@ -270,17 +264,17 @@ let build_beq_scheme mode kn =
Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
- let ar = Array.make n (Lazy.force ff) in
+ let ar = Array.make n (ff ()) in
let eff = ref Safe_typing.empty_private_constants in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
- let ar2 = Array.make n (Lazy.force ff) in
+ let ar2 = Array.make n (ff ()) in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
for j=0 to n-1 do
if Int.equal i j then
ar2.(j) <- let cc = (match nb_cstr_args with
- | 0 -> Lazy.force tt
- | _ -> let eqs = Array.make nb_cstr_args (Lazy.force tt) in
+ | 0 -> tt ()
+ | _ -> let eqs = Array.make nb_cstr_args (tt ()) in
for ndx = 0 to nb_cstr_args-1 do
let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
let eqA, eff' = compute_A_equality rel_list
@@ -305,7 +299,7 @@ let build_beq_scheme mode kn =
(constrsj.(j).cs_args)
)
else ar2.(j) <- (List.fold_left (fun a decl ->
- mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (Lazy.force ff) (constrsj.(j).cs_args) )
+ mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) )
done;
ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_name decl, RelDecl.get_type decl, a))
@@ -326,7 +320,7 @@ let build_beq_scheme mode kn =
for i=0 to (nb_ind-1) do
names.(i) <- Name (Id.of_string (rec_name i));
types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0)
- (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb));
+ (mkArrow (mkFullInd ((kn,i),u) 1) (bb ()));
let c, eff' = make_one_eq i in
cores.(i) <- c;
eff := Safe_typing.concat_private eff' !eff
@@ -570,15 +564,15 @@ let compute_bl_goal ind lnamesparrec nparrec =
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
mkArrow
- ( mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(mkVar seq,[|mkVar x;mkVar y|]);(Lazy.force tt)|]))
- ( mkApp(Lazy.force eq,[|mkVar s;mkVar x;mkVar y|]))
+ ( mkApp(eq (),[|bb (); mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt () |]))
+ ( mkApp(eq (),[|mkVar s;mkVar x;mkVar y|]))
))
) list_id in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
mkNamedProd sbl b a
) c (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
- mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(Lazy.force bb)))
+ mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,(bb ())))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
mkNamedProd seq b a
@@ -594,8 +588,8 @@ let compute_bl_goal ind lnamesparrec nparrec =
mkNamedProd n (mkFullInd (ind,u) nparrec) (
mkNamedProd m (mkFullInd (ind,u) (nparrec+1)) (
mkArrow
- (mkApp(Lazy.force eq,[|(Lazy.force bb);mkApp(eqI,[|mkVar n;mkVar m|]);(Lazy.force tt)|]))
- (mkApp(Lazy.force eq,[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
+ (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
+ (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
))), eff
let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
@@ -651,7 +645,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
| App (c,ca) -> (
match EConstr.kind sigma c with
| Ind (indeq, u) ->
- if GlobRef.equal (IndRef indeq) Coqlib.glob_eq
+ if GlobRef.equal (IndRef indeq) Coqlib.(lib_ref "core.eq.type")
then
Tacticals.New.tclTHEN
(do_replace_bl mode bl_scheme_key ind
@@ -704,7 +698,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
- let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
+ let eq = eq () and tt = tt () and bb = bb () in
let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let eqI, eff = eqI ind lnamesparrec in
let create_input c =
@@ -827,13 +821,13 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
(* Decidable equality *)
let check_not_is_defined () =
- try ignore (Coqlib.build_coq_not ())
- with e when CErrors.noncritical e -> raise (UndefinedCst "not")
+ try ignore (Coqlib.lib_ref "core.not.type")
+ with Not_found -> raise (UndefinedCst "not")
(* {n=m}+{n<>m} part *)
let compute_dec_goal ind lnamesparrec nparrec =
check_not_is_defined ();
- let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
+ let eq = eq () and tt = tt () and bb = bb () in
let list_id = list_id lnamesparrec in
let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
let create_input c =
@@ -879,14 +873,14 @@ let compute_dec_goal ind lnamesparrec nparrec =
create_input (
mkNamedProd n (mkFullInd ind (2*nparrec)) (
mkNamedProd m (mkFullInd ind (2*nparrec+1)) (
- mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|])
+ mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
)
)
)
let compute_dec_tact ind lnamesparrec nparrec =
- let eq = Lazy.force eq and tt = Lazy.force tt
- and ff = Lazy.force ff and bb = Lazy.force bb in
+ let eq = eq () and tt = tt ()
+ and ff = ff () and bb = bb () in
let list_id = list_id lnamesparrec in
let eqI, eff = eqI ind lnamesparrec in
let avoid = ref [] in
@@ -949,7 +943,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
simplest_right ;
- unfold_constr (Lazy.force Coqlib.coq_not_ref);
+ unfold_constr (Coqlib.lib_ref "core.not.type");
intro;
Equality.subst_all ();
assert_by (Name freshH3)
diff --git a/vernac/class.mli b/vernac/class.mli
index f7e837f3bb..80d6d4383c 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
val try_add_new_identity_coercion : Id.t -> local:bool ->
Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
-val add_coercion_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
-val add_subclass_hook : Decl_kinds.polymorphic -> unit Lemmas.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 37ee33b19f..09e2b8df45 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -149,7 +149,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if program_mode then
- let hook vis gr _ =
+ let hook _ vis gr =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false gr ~enriching:false [imps];
let pri = intern_info pri in
@@ -163,7 +163,7 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in obls, Some constr, typ
| None -> [||], None, termtype
in
- let hook = Lemmas.mk_hook hook in
+ let hook = Obligations.mk_univ_hook hook in
let ctx = Evd.evar_universe_context sigma in
ignore (Obligations.add_definition id ?term:constr
~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls)
@@ -425,7 +425,7 @@ let context poly l =
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
- let hook = Lemmas.mk_hook (fun _ gr -> gr) in
+ let hook = Lemmas.mk_hook (fun _ _ -> ()) in
let _ = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 60f9d67429..cc03473bc6 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -109,10 +109,8 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
Obligations.eterm_obligations env ident evd 0 c typ
in
let ctx = Evd.evar_universe_context evd in
- let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
+ let hook = Obligations.mk_univ_hook (fun _ l r -> Lemmas.call_hook (fun x -> x) hook l r) in
ignore(Obligations.add_definition
ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
- (Lemmas.mk_hook
- (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
+ ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps hook)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 7f1c902c0f..58007e6a88 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -19,7 +19,7 @@ open Constrexpr
val do_definition : program_mode:bool ->
Id.t -> definition_kind -> universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
- constr_expr option -> unit Lemmas.declaration_hook -> unit
+ constr_expr option -> Lemmas.declaration_hook -> unit
(************************************************************************)
(** Internal API *)
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 04cd4173a8..5f340dc144 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -160,14 +160,8 @@ type recursive_preentry =
(* Wellfounded definition *)
-let contrib_name = "Program"
-let subtac_dir = [contrib_name]
-let tactics_module = subtac_dir @ ["Tactics"]
-
-let init_constant dir s sigma =
- Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
-
-let fix_proto = init_constant tactics_module "fix_proto"
+let fix_proto sigma =
+ Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")
let interp_recursive ~program_mode ~cofix fixl notations =
let open Context.Named.Declaration in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 102a98f046..cea8af3f05 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -23,27 +23,16 @@ module RelDecl = Context.Rel.Declaration
open Coqlib
-let contrib_name = "Program"
-let subtac_dir = [contrib_name]
-let fixsub_module = subtac_dir @ ["Wf"]
-(* let tactics_module = subtac_dir @ ["Tactics"] *)
+let init_constant sigma rf = Evarutil.new_global sigma rf
+let fix_sub_ref () = lib_ref "program.wf.fix_sub"
+let measure_on_R_ref () = lib_ref "program.wf.mr"
+let well_founded sigma = init_constant sigma (lib_ref "core.wf.well_founded")
-let init_reference dir s () = Coqlib.coq_reference "Command" dir s
-let init_constant dir s sigma =
- Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)
-
-let make_ref l s = init_reference l s
-(* let fix_proto = init_constant tactics_module "fix_proto" *)
-let fix_sub_ref = make_ref fixsub_module "Fix_sub"
-let measure_on_R_ref = make_ref fixsub_module "MR"
-let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let mkSubset sigma name typ prop =
let open EConstr in
let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in
sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |])
-let sigT = Lazy.from_fun build_sigma_type
-
let make_qref s = qualid_of_string s
let lt_ref = make_qref "Init.Peano.lt"
@@ -60,8 +49,8 @@ let rec telescope sigma l =
(fun (sigma, ty, tys, (k, constr)) decl ->
let t = RelDecl.get_type decl in
let pred = mkLambda (RelDecl.get_name decl, t, ty) in
- let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in
- let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in
+ let sigma, ty = Evarutil.new_global sigma (lib_ref "core.sigT.type") in
+ let sigma, intro = Evarutil.new_global sigma (lib_ref "core.sigT.intro") in
let sigty = mkApp (ty, [|t; pred|]) in
let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
(sigma, sigty, pred :: tys, (succ k, intro)))
@@ -70,8 +59,8 @@ let rec telescope sigma l =
let sigma, last, subst = List.fold_right2
(fun pred decl (sigma, prev, subst) ->
let t = RelDecl.get_type decl in
- let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in
- let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in
+ let sigma, p1 = Evarutil.new_global sigma (lib_ref "core.sigT.proj1") in
+ let sigma, p2 = Evarutil.new_global sigma (lib_ref "core.sigT.proj2") in
let proj1 = applist (p1, [t; pred; prev]) in
let proj2 = applist (p2, [t; pred; prev]) in
(sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
@@ -203,7 +192,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let name = add_suffix recname "_func" in
(* XXX: Mutating the evar_map in the hook! *)
(* XXX: Likely the sigma is out of date when the hook is called .... *)
- let hook sigma l gr _ =
+ let hook sigma _ l gr =
let sigma, h_body = Evarutil.new_global sigma gr in
let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
@@ -222,13 +211,13 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
hook, name, typ
else
let typ = it_mkProd_or_LetIn top_arity binders_rel in
- let hook sigma l gr _ =
+ let hook sigma _ l gr =
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in hook, recname, typ
in
(* XXX: Capturing sigma here... bad bad *)
- let hook = Lemmas.mk_hook (hook sigma) in
+ let hook = Obligations.mk_univ_hook (hook sigma) in
(* XXX: Grounding non-ground terms here... bad bad *)
let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
@@ -255,7 +244,7 @@ let do_program_recursive local poly fixkind fixl ntns =
interp_recursive ~cofix ~program_mode:true fixl ntns
in
(* Program-specific code *)
- (* Get the interesting evars, those that were not instanciated *)
+ (* Get the interesting evars, those that were not instantiated *)
let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
(* Solve remaining evars *)
let evd = nf_evar_map_undefined evd in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 77177dfa41..35fb18e292 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,34 +33,22 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_global_definition ident ce local k pl imps =
- let local = get_locality ident ~kind:"definition" local in
- let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
- let gr = ConstRef kn in
- let () = maybe_declare_manual_implicits false gr imps in
- let () = Declare.declare_univ_binders gr pl in
- let () = definition_message ident in
- gr
-
let declare_definition ident (local, p, k) ce pl imps hook =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
- let r = match local with
+ let gr = match local with
| Discharge when Lib.sections_are_opened () ->
- let c = SectionLocalDef ce in
- let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
- let () = definition_message ident in
- let gr = VarRef ident in
- let () = maybe_declare_manual_implicits false gr imps in
- let () = Declare.declare_univ_binders gr pl in
- let () = if Proof_global.there_are_pending_proofs () then
- warn_definition_not_visible ident
- in
- gr
+ let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
+ let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in
+ VarRef ident
| Discharge | Local | Global ->
- declare_global_definition ident ce local k pl imps in
- Lemmas.call_hook fix_exn hook local r
+ let local = get_locality ident ~kind:"definition" local in
+ let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+ ConstRef kn in
+ let () = maybe_declare_manual_implicits false gr imps in
+ let () = Declare.declare_univ_binders gr pl in
+ let () = definition_message ident in
+ Lemmas.call_hook fix_exn hook local gr; gr
let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
-
+ declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ()))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index c5e704a5e9..da11d4d9c0 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,7 +15,7 @@ val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits ->
- GlobRef.t Lemmas.declaration_hook -> GlobRef.t
+ Lemmas.declaration_hook -> GlobRef.t
val declare_fix : ?opaque:bool -> definition_kind ->
UnivNames.universe_binders -> Entries.constant_universes_entry ->
diff --git a/vernac/egramml.ml b/vernac/egramml.ml
index c5dedc880e..89caff847f 100644
--- a/vernac/egramml.ml
+++ b/vernac/egramml.ml
@@ -19,7 +19,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- ('a raw_abstract_argument_type option * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
+ ('a raw_abstract_argument_type * ('s, 'a) symbol) Loc.located -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
@@ -40,7 +40,7 @@ let rec ty_rule_of_gram = function
AnyTyRule r
| GramNonTerminal (_, (t, tok)) :: rem ->
let AnyTyRule rem = ty_rule_of_gram rem in
- let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
+ let inj = Some (fun obj -> Genarg.in_gen t obj) in
let r = TyNext (rem, tok, inj) in
AnyTyRule r
diff --git a/vernac/egramml.mli b/vernac/egramml.mli
index c4f4fcfaa4..a90ef97e7d 100644
--- a/vernac/egramml.mli
+++ b/vernac/egramml.mli
@@ -17,7 +17,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal : ('a Genarg.raw_abstract_argument_type option *
+ | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item
val extend_vernac_command_grammar :
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 895737b538..d7229d32fe 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,7 +212,7 @@ GRAMMAR EXTEND Gram
| IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
| IDENT "Register"; g = global; "as"; quid = qualid ->
- { VernacRegister(g, RegisterRetroknowledge quid) }
+ { VernacRegister(g, RegisterCoqlib quid) }
| IDENT "Register"; IDENT "Inline"; g = global ->
{ VernacRegister(g, RegisterInline) }
| IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
@@ -994,7 +994,9 @@ GRAMMAR EXTEND Gram
| IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) }
| IDENT "All"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, true, qid) }
| IDENT "Strategy"; qid = smart_global -> { PrintStrategy (Some qid) }
- | IDENT "Strategies" -> { PrintStrategy None } ] ]
+ | IDENT "Strategies" -> { PrintStrategy None }
+ | IDENT "Registered" -> { PrintRegistered }
+ ] ]
;
class_rawexpr:
[ [ IDENT "Funclass" -> { FunClass }
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index b354ad0521..5f2818c12b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -451,11 +451,11 @@ let fold_left' f = function
[] -> invalid_arg "fold_left'"
| hd :: tl -> List.fold_left f hd tl
-let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ())
-let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ())
+let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.and.type")
+let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.and.conj")
-let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.build_coq_prod ())
-let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.build_coq_pair ())
+let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.type")
+let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.intro")
let build_combined_scheme env schemes =
let evdref = ref (Evd.from_env env) in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4f0bf1b5d2..8aa459729c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -34,7 +34,7 @@ open Impargs
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type 'a declaration_hook = Decl_kinds.locality -> GlobRef.t -> 'a
+type declaration_hook = Decl_kinds.locality -> GlobRef.t -> unit
let mk_hook hook = hook
let call_hook fix_exn hook l c =
try hook l c
@@ -179,14 +179,14 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
let const = adjust_guardness_conditions const do_guard in
let k = Kindops.logical_kind_of_goal_kind kind in
let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
- let l,r = match locality with
+ let r = match locality with
| Discharge when Lib.sections_are_opened () ->
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
let () = if should_suggest
then Proof_using.suggest_variable (Global.env ()) id
in
- (Local, VarRef id)
+ VarRef id
| Local | Global | Discharge ->
let local = match locality with
| Local | Discharge -> true
@@ -197,11 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
let () = if should_suggest
then Proof_using.suggest_constant (Global.env ()) kn
in
- (locality, ConstRef kn)
+ ConstRef kn
in
definition_message id;
Declare.declare_univ_binders r (UState.universe_binders uctx);
- call_hook (fun exn -> exn) hook l r
+ call_hook (fun exn -> exn) hook locality r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
iraise (fix_exn e)
@@ -221,12 +221,12 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
+ let k = IsAssumption Conjectural in
match body with
| None ->
(match locality with
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
- let k = IsAssumption Conjectural in
let univs = match univs with
| Polymorphic_const_entry univs ->
(* What is going on here? *)
@@ -237,7 +237,6 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
let _ = declare_variable id (Lib.cwd(),c,k) in
(Discharge, VarRef id,imps)
| Local | Global ->
- let k = IsAssumption Conjectural in
let local = match locality with
| Local -> true
| Global -> false
@@ -277,22 +276,10 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality,ConstRef kn,imps)
-let save_hook = ref ignore
-let set_save_hook f = save_hook := f
-
-let save_named ?export_seff proof =
- let id,const,uctx,do_guard,persistence,hook = proof in
- save ?export_seff id const uctx do_guard persistence hook
-
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
user_err Pp.(str "This command can only be used for unnamed theorem.")
-let save_anonymous ?export_seff proof save_ident =
- let id,const,uctx,do_guard,persistence,hook = proof in
- check_anonymity id save_ident;
- save ?export_seff save_ident const uctx do_guard persistence hook
-
(* Admitted *)
let warn_let_as_axiom =
@@ -312,16 +299,6 @@ let admit (id,k,e) pl hook () =
(* Starting a goal *)
-let start_hook = ref ignore
-let set_start_hook = (:=) start_hook
-
-
-let get_proof proof do_guard hook opacity =
- let (id,(const,univs,persistence)) =
- Pfedit.cook_this_proof proof
- in
- id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
@@ -333,12 +310,12 @@ let universe_proof_terminator compute_guard hook =
| Transparent -> false, true
| Opaque -> true, false
in
- let proof = get_proof proof compute_guard
- (hook (Some (proof.Proof_global.universes))) is_opaque in
- begin match idopt with
- | None -> save_named ~export_seff proof
- | Some { CAst.v = id } -> save_anonymous ~export_seff proof id
- end
+ let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in
+ let const = {const with const_entry_opaque = is_opaque} in
+ let id = match idopt with
+ | None -> id
+ | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+ save ~export_seff id const univs compute_guard persistence (hook (Some univs))
end
let standard_proof_terminator compute_guard hook =
@@ -362,7 +339,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=
| Some sign -> sign
| None -> initialize_named_context_for_proof ()
in
- !start_hook c;
Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
@@ -375,7 +351,6 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
| Some sign -> sign
| None -> initialize_named_context_for_proof ()
in
- !start_hook c;
Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
let rec_tac_initializer finite guard thms snl =
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 62b25946d9..195fcbf4ca 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,47 +11,41 @@
open Names
open Decl_kinds
-type 'a declaration_hook
-val mk_hook :
- (Decl_kinds.locality -> GlobRef.t -> 'a) -> 'a declaration_hook
-
-val call_hook :
- Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a
-
-(** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (EConstr.types -> unit) -> unit
+type declaration_hook
+val mk_hook : (Decl_kinds.locality -> GlobRef.t -> unit) -> declaration_hook
+val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> GlobRef.t -> unit
val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
+ ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
- unit declaration_hook -> unit
+ ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+ declaration_hook -> unit
val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
- ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
+ ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) ->
?sign:Environ.named_context_val -> EConstr.types ->
- ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
- (UState.t option -> unit declaration_hook) -> unit
+ ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards ->
+ (UState.t option -> declaration_hook) -> unit
val start_proof_com :
?inference_hook:Pretyping.inference_hook ->
goal_kind -> Vernacexpr.proof_expr list ->
- unit declaration_hook -> unit
+ declaration_hook -> unit
val start_proof_with_initialization :
goal_kind -> Evd.evar_map -> UState.universe_decl ->
(bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
(Id.t (* name of thm *) *
(EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
- -> int list option -> unit declaration_hook -> unit
+ -> int list option -> declaration_hook -> unit
val universe_proof_terminator :
Proof_global.lemma_possible_guards ->
- (UState.t option -> unit declaration_hook) ->
+ (UState.t option -> declaration_hook) ->
Proof_global.proof_terminator
val standard_proof_terminator :
- Proof_global.lemma_possible_guards -> unit declaration_hook ->
+ Proof_global.lemma_possible_guards -> declaration_hook ->
Proof_global.proof_terminator
val fresh_name_for_anonymous_theorem : unit -> Id.t
@@ -63,7 +57,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
(** {6 ... } *)
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.t -> unit) -> unit
-
val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c4a10b4be6..5352cf5f8c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -20,6 +20,14 @@ open Pp
open CErrors
open Util
+type univ_declaration_hook = UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+let mk_univ_hook f = f
+let call_univ_hook fix_exn hook uctx l c =
+ try hook uctx l c
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
+ iraise (fix_exn e)
+
module NamedDecl = Context.Named.Declaration
let get_fix_exn, stm_get_fix_exn = Hook.make ()
@@ -256,11 +264,9 @@ let eterm_obligations env name evm fs ?status t ty =
let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
Array.of_list (List.rev evars), (evnames, evmap), t', ty
-let tactics_module = ["Program";"Tactics"]
-let safe_init_constant md name () =
- Coqlib.check_required_library ("Coq"::md);
- UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
-let hide_obligation = safe_init_constant tactics_module "obligation"
+let hide_obligation () =
+ Coqlib.check_required_library ["Coq";"Program";"Tactics"];
+ UnivGen.constr_of_global (Coqlib.lib_ref "program.tactics.obligation")
let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)
@@ -316,7 +322,7 @@ type program_info_aux = {
prg_notations : notations ;
prg_kind : definition_kind;
prg_reduce : constr -> constr;
- prg_hook : (UState.t -> unit) Lemmas.declaration_hook;
+ prg_hook : univ_declaration_hook;
prg_opaque : bool;
prg_sign: named_context_val;
}
@@ -342,7 +348,7 @@ open Goptions
let _ =
declare_bool_option
{ optdepr = false;
- optname = "Hidding of Program obligations";
+ optname = "Hiding of Program obligations";
optkey = ["Hide";"Obligations"];
optread = get_hide_obligations;
optwrite = set_hide_obligations; }
@@ -490,7 +496,7 @@ let declare_definition prg =
let ubinders = UState.universe_binders uctx in
DeclareDef.declare_definition prg.prg_name
prg.prg_kind ce ubinders prg.prg_implicits
- (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r))
+ (Lemmas.mk_hook (fun l r -> call_univ_hook fix_exn prg.prg_hook uctx l r ; ()))
let rec lam_index n t acc =
match Constr.kind t with
@@ -564,7 +570,7 @@ let declare_mutual_definition l =
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
let gr = List.hd kns in
- Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+ call_univ_hook fix_exn first.prg_hook first.prg_ctx local gr;
List.iter progmap_remove l; gr
let decompose_lam_prod c ty =
@@ -1101,7 +1107,7 @@ let show_term n =
let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
+ ?(reduce=reduce) ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
let sign = Lemmas.initialize_named_context_for_proof () in
let info = Id.print n ++ str " has type-checked" in
let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce hook in
@@ -1121,7 +1127,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
?(kind=Global,false,Definition) ?(reduce=reduce)
- ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
+ ?(hook=mk_univ_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
let sign = Lemmas.initialize_named_context_for_proof () in
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a37c30aafc..80294c7a76 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,6 +13,10 @@ open Constr
open Evd
open Names
+type univ_declaration_hook
+val mk_univ_hook : (UState.t -> Decl_kinds.locality -> GlobRef.t -> unit) -> univ_declaration_hook
+val call_univ_hook : Future.fix_exn -> univ_declaration_hook -> UState.t -> Decl_kinds.locality -> GlobRef.t -> unit
+
(* This is a hack to make it possible for Obligations to craft a Qed
* behind the scenes. The fix_exn the Stm attaches to the Future proof
* is not available here, so we provide a side channel to get it *)
@@ -59,7 +63,7 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
?reduce:(constr -> constr) ->
- ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
+ ?hook:univ_declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
(lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -76,7 +80,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(constr -> constr) ->
- ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool ->
+ ?hook:univ_declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b4b3aead91..a0e8f38c0b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -533,6 +533,8 @@ open Pputils
keyword "Print Strategies"
| PrintStrategy (Some qid) ->
keyword "Print Strategy" ++ pr_smart_global qid
+ | PrintRegistered ->
+ keyword "Print Registered"
let pr_using e =
let rec aux = function
@@ -1159,14 +1161,16 @@ open Pputils
| LocateOther (s, qid) -> keyword s ++ spc () ++ pr_ltac_ref qid
in
return (keyword "Locate" ++ spc() ++ pr_locate loc)
- | VernacRegister (id, RegisterInline) ->
+ | VernacRegister (qid, RegisterCoqlib name) ->
return (
hov 2
- (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+ (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
+ ++ spc () ++ pr_qualid name)
)
- | VernacRegister (id, RegisterRetroknowledge n) ->
+ | VernacRegister (qid, RegisterInline) ->
return (
- hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ pr_qualid n)
+ hov 2
+ (keyword "Register Inline" ++ spc() ++ pr_qualid qid)
)
| VernacComments l ->
return (
diff --git a/vernac/search.ml b/vernac/search.ml
index e8ccec11ca..04dcb7d565 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -236,13 +236,13 @@ let search_pattern gopt pat mods pr_search =
(** SearchRewrite *)
-let eq = Coqlib.glob_eq
+let eq () = Coqlib.(lib_ref "core.eq.type")
let rewrite_pat1 pat =
- PApp (PRef eq, [| PMeta None; pat; PMeta None |])
+ PApp (PRef (eq ()), [| PMeta None; pat; PMeta None |])
let rewrite_pat2 pat =
- PApp (PRef eq, [| PMeta None; PMeta None; pat |])
+ PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
let search_rewrite gopt pat mods pr_search =
let pat1 = rewrite_pat1 pat in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index cf2fecb9c1..48d4165830 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -311,6 +311,13 @@ let print_strategy r =
let lvl = get_strategy oracle key in
pr_strategy (r, lvl)
+let print_registered () =
+ let pr_lib_ref (s,r) =
+ pr_global r ++ str " registered as " ++ str s
+ in
+ hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
+
+
let dump_universes_gen g s =
let output = open_out s in
let output_constraint, close =
@@ -472,10 +479,12 @@ let start_proof_and_print k l hook =
let no_hook = Lemmas.mk_hook (fun _ _ -> ())
let vernac_definition_hook p = function
-| Coercion -> Class.add_coercion_hook p
+| Coercion ->
+ Class.add_coercion_hook p
| CanonicalStructure ->
- Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
-| SubClass -> Class.add_subclass_hook p
+ Lemmas.mk_hook (fun _ -> Recordops.declare_canonical_structure)
+| SubClass ->
+ Class.add_subclass_hook p
| _ -> no_hook
let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
@@ -1866,6 +1875,7 @@ let vernac_print ~atts env sigma =
Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in
Printer.pr_assumptionset env sigma nassums
| PrintStrategy r -> print_strategy r
+ | PrintRegistered -> print_registered ()
let global_module qid =
try Nametab.full_name_module qid
@@ -1972,14 +1982,14 @@ let vernac_register qid r =
if not (isConstRef gr) then
user_err Pp.(str "Register inline: a constant is expected");
Global.register_inline (destConstRef gr)
- | RegisterRetroknowledge n ->
+ | RegisterCoqlib 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))
+ Coqlib.register_ref (Libnames.string_of_qualid n) gr
(********************)
(* Proof management *)
@@ -2226,7 +2236,7 @@ let interp ?proof ~atts ~st c =
| VernacSearch (s,g,r) -> vernac_search ~atts s g r
| VernacLocate l ->
Feedback.msg_notice @@ vernac_locate l
- | VernacRegister (id, r) -> vernac_register id r
+ | VernacRegister (qid, r) -> vernac_register qid r
| VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
(* Proof management *)
@@ -2278,6 +2288,7 @@ let check_vernac_supports_locality c l =
| VernacSetOption _ | VernacUnsetOption _
| VernacDeclareReduction _
| VernacExtend _
+ | VernacRegister _
| VernacInductive _) -> ()
| Some _, _ -> user_err Pp.(str "This command does not support Locality")
@@ -2496,8 +2507,7 @@ type classifier = Genarg.raw_generic_argument list -> vernac_classification
type (_, _) ty_sig =
| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
-| TyNonTerminal :
- string option * ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
+| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
@@ -2510,7 +2520,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio
| _ :: _ -> type_error ()
end
| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args
-| TyNonTerminal (_, tu, ty) -> fun f args ->
+| TyNonTerminal (tu, ty) -> fun f args ->
begin match args with
| [] -> type_error ()
| Genarg.GenArg (Rawwit tag, v) :: args ->
@@ -2527,7 +2537,7 @@ let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_comm
| _ :: _ -> type_error ()
end
| TyTerminal (_, ty) -> fun f args -> untype_command ty f args
-| TyNonTerminal (_, tu, ty) -> fun f args ->
+| TyNonTerminal (tu, ty) -> fun f args ->
begin match args with
| [] -> type_error ()
| Genarg.GenArg (Rawwit tag, v) :: args ->
@@ -2548,8 +2558,8 @@ let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s
let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function
| TyNil -> []
| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty
-| TyNonTerminal (id, tu, ty) ->
- let t = Option.map (fun _ -> rawwit (Egramml.proj_symbol tu)) id in
+| TyNonTerminal (tu, ty) ->
+ let t = rawwit (Egramml.proj_symbol tu) in
let symb = untype_user_symbol tu in
Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty
@@ -2603,3 +2613,30 @@ let vernac_extend ~command ?classifier ?entry ext =
in
let () = declare_vernac_classifier command cl in
List.iteri iter ext
+
+(** VERNAC ARGUMENT EXTEND registering *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+| Arg_rules of 'a Extend.production_rule list
+
+type 'a vernac_argument = {
+ arg_printer : 'a -> Pp.t;
+ arg_parsing : 'a argument_rule;
+}
+
+let vernac_argument_extend ~name arg =
+ let wit = Genarg.create_arg name in
+ let entry = match arg.arg_parsing with
+ | Arg_alias e ->
+ let () = Pcoq.register_grammar wit e in
+ e
+ | Arg_rules rules ->
+ let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+ let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in
+ e
+ in
+ let pr = arg.arg_printer in
+ let pr x = Genprint.PrinterBasic (fun () -> pr x) in
+ let () = Genprint.register_vernac_print0 wit pr in
+ (wit, entry)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index fb2a30bac7..0c4630e45f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -51,7 +51,6 @@ type (_, _) ty_sig =
| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
| TyNonTerminal :
- string option *
('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
('a -> 'r, 'a -> 's) ty_sig
@@ -64,6 +63,24 @@ val vernac_extend :
?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
ty_ml list -> unit
+(** {5 VERNAC ARGUMENT EXTEND} *)
+
+type 'a argument_rule =
+| Arg_alias of 'a Pcoq.Entry.t
+ (** This is used because CAMLP5 parser can be dumb about rule factorization,
+ which sometimes requires two entries to be the same. *)
+| Arg_rules of 'a Extend.production_rule list
+ (** There is a discrepancy here as we use directly extension rules and thus
+ entries instead of ty_user_symbol and thus arguments as roots. *)
+
+type 'a vernac_argument = {
+ arg_printer : 'a -> Pp.t;
+ arg_parsing : 'a argument_rule;
+}
+
+val vernac_argument_extend : name:string -> 'a vernac_argument ->
+ ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
+
(** {5 STM classifiers} *)
val get_vernac_classifier :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index a2ea706b75..27b485d94d 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -57,6 +57,7 @@ type printable =
| PrintImplicit of qualid or_by_notation
| PrintAssumptions of bool * bool * qualid or_by_notation
| PrintStrategy of qualid or_by_notation option
+ | PrintRegistered
type search_about_item =
| SearchSubPattern of constr_pattern_expr
@@ -230,7 +231,7 @@ type extend_name =
It will be extended with primitive inductive types and operators *)
type register_kind =
| RegisterInline
- | RegisterRetroknowledge of qualid
+ | RegisterCoqlib of qualid
(** {6 Types concerning the module layer} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 23:28:23 +0000