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/firstorder/g_ground.ml4 | 6 +++--- plugins/firstorder/rules.ml | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 7e54bc8adb..fdeef5f0ac 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -109,11 +109,11 @@ let gen_ground_tac flag taco ids bases = (* special for compatibility with Intuition -let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str +let constant str = Coqlib.get_constr str let defined_connectives=lazy - [[],EvalConstRef (destConst (constant "not")); - [],EvalConstRef (destConst (constant "iff"))] + [[],EvalConstRef (destConst (constant "core.not.type")); + [],EvalConstRef (destConst (constant "core.iff.type"))] let normalize_evaluables= onAllHypsAndConcl diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 3ae777cc9a..8fa676de44 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -234,11 +234,11 @@ let ll_forall_tac prod backtrack id continue seq= (* special for compatibility with old Intuition *) let constant str = UnivGen.constr_of_global - @@ Coqlib.coq_reference "User" ["Init";"Logic"] str + @@ Coqlib.lib_ref str -let defined_connectives=lazy - [AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "not"))); - AllOccurrences,EvalConstRef (fst (Constr.destConst (constant "iff")))] +let defined_connectives = lazy + [AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.not.type"))); + AllOccurrences, EvalConstRef (fst (Constr.destConst (constant "core.iff.type")))] let normalize_evaluables= Proofview.Goal.enter begin fun gl -> -- cgit v1.2.3