diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 50 |
1 files changed, 12 insertions, 38 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 4eee2c7a45..28a9542167 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -114,8 +114,9 @@ let def_of_const t = with Not_found -> assert false) |_ -> assert false +[@@@ocaml.warning "-3"] let coq_constant s = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -297,36 +298,7 @@ let subst_Function (subst,finfos) = let classify_Function infos = Libobject.Substitute infos -let discharge_Function (_,finfos) = - let function_constant' = Lib.discharge_con finfos.function_constant - and graph_ind' = Lib.discharge_inductive finfos.graph_ind - and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma - in - if function_constant' == finfos.function_constant && - graph_ind' == finfos.graph_ind && - equation_lemma' == finfos.equation_lemma && - correctness_lemma' == finfos.correctness_lemma && - completeness_lemma' == finfos.completeness_lemma && - rect_lemma' == finfos.rect_lemma && - rec_lemma' == finfos.rec_lemma && - prop_lemma' == finfos.prop_lemma - then Some finfos - else - Some { function_constant = function_constant' ; - graph_ind = graph_ind' ; - equation_lemma = equation_lemma' ; - correctness_lemma = correctness_lemma' ; - completeness_lemma = completeness_lemma'; - rect_lemma = rect_lemma'; - rec_lemma = rec_lemma'; - prop_lemma = prop_lemma' ; - is_general = finfos.is_general - } +let discharge_Function (_,finfos) = Some finfos let pr_ocst c = let sigma, env = Pfedit.get_current_context () in @@ -339,7 +311,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr_env env sigma - (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) + (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -469,16 +441,16 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" + UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" + UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -490,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") -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" +[@@@ocaml.warning "-3"] +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ + 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") |