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/cc/cctac.ml | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2eaa6146e1..055d36747d 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -28,17 +28,13 @@ open Proofview.Notations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -let reference dir s = lazy (Coqlib.coq_reference "CC" dir s) - -let _f_equal = reference ["Init";"Logic"] "f_equal" -let _eq_rect = reference ["Init";"Logic"] "eq_rect" -let _refl_equal = reference ["Init";"Logic"] "eq_refl" -let _sym_eq = reference ["Init";"Logic"] "eq_sym" -let _trans_eq = reference ["Init";"Logic"] "eq_trans" -let _eq = reference ["Init";"Logic"] "eq" -let _False = reference ["Init";"Logic"] "False" -let _True = reference ["Init";"Logic"] "True" -let _I = reference ["Init";"Logic"] "I" +let _f_equal = lazy (Coqlib.lib_ref "core.eq.congr") +let _eq_rect = lazy (Coqlib.lib_ref "core.eq.rect") +let _refl_equal = lazy (Coqlib.lib_ref "core.eq.refl") +let _sym_eq = lazy (Coqlib.lib_ref "core.eq.sym") +let _trans_eq = lazy (Coqlib.lib_ref "core.eq.trans") +let _eq = lazy (Coqlib.lib_ref "core.eq.type") +let _False = lazy (Coqlib.lib_ref "core.False.type") let whd env sigma t = Reductionops.clos_whd_flags CClosure.betaiotazeta env sigma t @@ -423,7 +419,7 @@ let build_term_to_complete uf pac = let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in - Coqlib.check_required_library Coqlib.logic_module_name; + Coqlib.(check_required_library logic_module_name); let _ = debug (fun () -> Pp.str "Reading subgoal ...") in let state = make_prb gl depth additionnal_terms in let _ = debug (fun () -> Pp.str "Problem built, solving ...") in -- cgit v1.2.3