diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 27 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 46 |
2 files changed, 30 insertions, 43 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 45fafd2872..7d87fc0220 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -92,18 +92,14 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l -[@@@ocaml.warning "-3"] -let coq_constant s = - UnivGen.constr_of_monomorphic_global @@ - Coqlib.gen_reference_in_modules "RecursiveDefinition" - Coqlib.init_modules s;; +let coq_constant s = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in Nametab.locate (make_qualid dp (Id.of_string s)) -let eq = lazy(EConstr.of_constr (coq_constant "eq")) -let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) +let eq = lazy(EConstr.of_constr (coq_constant "core.eq.type")) +let refl_equal = lazy(EConstr.of_constr (coq_constant "core.eq.refl")) let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () @@ -369,10 +365,10 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in if not (Stack.is_empty debug_queue) then print_debug_queue true (fst reraise); - Util.iraise reraise + Exninfo.iraise reraise let observe_tac s tac g = if do_observe () @@ -447,14 +443,11 @@ let h_intros l = let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" -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_monomorphic_global @@ - Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" -[@@@ocaml.warning "+3"] +let well_founded = function () -> EConstr.of_constr (coq_constant "core.wf.well_founded") +let acc_rel = function () -> EConstr.of_constr (coq_constant "core.wf.acc") +let acc_inv_id = function () -> EConstr.of_constr (coq_constant "core.wf.acc_inv") + +let well_founded_ltof () = EConstr.of_constr (coq_constant "num.nat.well_founded_ltof") let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f7f8004998..9fa0ec8c08 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -47,18 +47,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -[@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ - Coqlib.find_reference "RecursiveDefinition" m s - -let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Coq"; "Arith";"Lt"] +let coq_constant s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref s let coq_init_constant s = - EConstr.of_constr ( - UnivGen.constr_of_monomorphic_global @@ - Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) -[@@@ocaml.warning "+3"] + EConstr.of_constr(UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s) +;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -122,26 +116,26 @@ let v_id = Id.of_string "v" let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; -let lt = function () -> (coq_init_constant "lt") -[@@@ocaml.warning "-3"] -let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") -let ex = function () -> (coq_init_constant "ex") -let nat = function () -> (coq_init_constant "nat") +let lt = function () -> (coq_init_constant "num.nat.lt") +let le = function () -> Coqlib.lib_ref "num.nat.le" + +let ex = function () -> (coq_init_constant "core.ex.type") +let nat = function () -> (coq_init_constant "num.nat.type") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref)) -let eq = function () -> (coq_init_constant "eq") +let eq = function () -> (coq_init_constant "core.eq.type") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") -let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") -let le_trans = function () -> (coq_constant arith_Nat "le_trans") -let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans") -let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n") -let le_n = function () -> (coq_init_constant "le_n") +let le_lt_n_Sm = function () -> (coq_constant "num.nat.le_lt_n_Sm") +let le_trans = function () -> (coq_constant "num.nat.le_trans") +let le_lt_trans = function () -> (coq_constant "num.nat.le_lt_trans") +let lt_S_n = function () -> (coq_constant "num.nat.lt_S_n") +let le_n = function () -> (coq_init_constant "num.nat.le_n") let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") -let coq_O = function () -> (coq_init_constant "O") -let coq_S = function () -> (coq_init_constant "S") -let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") +let coq_O = function () -> (coq_init_constant "num.nat.O") +let coq_S = function () -> (coq_init_constant"num.nat.S") +let lt_n_O = function () -> (coq_constant "num.nat.nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref)) @@ -817,7 +811,7 @@ let rec prove_le g = | App (c, [| x0 ; _ |]) -> EConstr.isVar sigma x0 && Id.equal (destVar sigma x0) (destVar sigma x) && - EConstr.is_global sigma (le ()) c + EConstr.isRefX sigma (le ()) c | _ -> false in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in @@ -1194,7 +1188,7 @@ let get_current_subgoals_types pstate = exception EmptySubgoals let build_and_l sigma l = let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in - let conj_constr = Coqlib.build_coq_conj () in + let conj_constr = Coqlib.lib_ref "core.and.conj" in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = |