From 8ac6145d5cc14823df48698a755d8adf048f026c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2017 12:22:32 +0200 Subject: [coqlib] Rebindable Coqlib namespace. We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- plugins/funind/recdef.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'plugins/funind/recdef.ml') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 633d98a585..89dfb58017 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -49,11 +49,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) +[@@@ocaml.warning "-3"] let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "RecursiveDefinition" m s + Coqlib.find_reference "RecursiveDefinition" m s -let arith_Nat = ["Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Arith";"Lt"] +let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] +let arith_Lt = ["Coq"; "Arith";"Lt"] let pr_leconstr_rd = let sigma, env = Pfedit.get_current_context () in @@ -63,6 +64,7 @@ let coq_init_constant s = EConstr.of_constr ( UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) +[@@@ocaml.warning "+3"] let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -143,6 +145,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") +[@@@ocaml.warning "-3"] let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") @@ -163,7 +166,6 @@ let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) -let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -1241,8 +1243,8 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.build_coq_and () in - let conj_constr = coq_conj () in + let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" in + let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = -- cgit v1.2.3