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/funind/indfun_common.ml | |
| parent | 96b30e352ff30b1fba4f11b278f22aa6db5871f9 (diff) | |
| parent | 8ac6145d5cc14823df48698a755d8adf048f026c (diff) | |
Merge PR #186: [RFC] Coqlib cleanup
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6ed382ca1c..03a64988e4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -114,6 +114,7 @@ let def_of_const t = with Not_found -> assert false) |_ -> assert false +[@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" @@ -441,7 +442,7 @@ let jmeq () = Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" + Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = @@ -449,7 +450,7 @@ let jmeq_refl () = Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" + Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -461,8 +462,10 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded" let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") +[@@@ocaml.warning "-3"] let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" + Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" +[@@@ocaml.warning "+3"] let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") |