diff options
| author | Pierre-Marie Pédrot | 2018-10-11 14:27:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-11 14:27:29 +0200 |
| commit | aa5cdbd67b160417fe353a79393a89ed99481548 (patch) | |
| tree | 3104f09c8af83b2726530a4ed64175a3f179bad0 /plugins/cc | |
| parent | 96b30e352ff30b1fba4f11b278f22aa6db5871f9 (diff) | |
| parent | 8ac6145d5cc14823df48698a755d8adf048f026c (diff) | |
Merge PR #186: [RFC] Coqlib cleanup
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 20 |
1 files changed, 8 insertions, 12 deletions
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 |