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/rules.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/firstorder/rules.ml') 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