diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 96 |
1 files changed, 22 insertions, 74 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a0b9217c75..c864bfe9f7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -27,13 +27,7 @@ let array_get_start a = (Array.length a - 1) (fun i -> a.(i)) -let id_of_name = function - Name id -> id - | _ -> raise Not_found - -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with @@ -107,17 +101,9 @@ let const_of_id id = CErrors.user_err ~hdr:"IndFun.const_of_id" (str "cannot find " ++ Id.print id) -let def_of_const t = - match Constr.kind t with - Term.Const sp -> - (try (match Environ.constant_opt_value_in (Global.env()) sp with - | Some c -> c - | _ -> assert false) - with Not_found -> assert false) - |_ -> assert false - +[@@@ocaml.warning "-3"] let coq_constant s = - Universes.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -161,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook = CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id - - -let cook_proof _ = - let (id,(entry,_,strength)) = Pfedit.cook_proof () in - (id,(entry,strength)) - -let get_proof_clean do_reduce = - let result = cook_proof do_reduce in - Proof_global.discard_current (); - result - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () @@ -269,12 +244,12 @@ let subst_Function (subst,finfos) = in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in - let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in - let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in - let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in - let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in - let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in - let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in + let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in + let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in + let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in + let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in + let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in + let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -299,36 +274,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.smartmap Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Option.smartmap 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 @@ -341,7 +287,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 () ++ @@ -429,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig = optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) } -let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true @@ -442,7 +388,7 @@ let function_debug_sig = optwrite = (fun b -> function_debug := b) } -let _ = declare_bool_option function_debug_sig +let () = declare_bool_option function_debug_sig let do_observe () = !function_debug @@ -460,7 +406,7 @@ let strict_tcc_sig = optwrite = (fun b -> strict_tcc := b) } -let _ = declare_bool_option strict_tcc_sig +let () = declare_bool_option strict_tcc_sig exception Building_graph of exn @@ -471,16 +417,16 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.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 @@ - Universes.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 = @@ -492,8 +438,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 @@ Universes.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") |