diff options
| -rw-r--r-- | plugins/funind/indfun_common.ml | 27 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 46 | ||||
| -rw-r--r-- | theories/Arith/Lt.v | 8 | ||||
| -rw-r--r-- | theories/Arith/PeanoNat.v | 3 | ||||
| -rw-r--r-- | theories/Arith/Wf_nat.v | 2 | ||||
| -rw-r--r-- | theories/Init/Peano.v | 2 | ||||
| -rw-r--r-- | theories/Init/Wf.v | 3 |
7 files changed, 48 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 = diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 918b0efc5a..8904f3f936 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -41,11 +41,15 @@ Proof. apply Nat.lt_succ_r. Qed. +Register lt_n_Sm_le as num.nat.lt_n_Sm_le. + Theorem le_lt_n_Sm n m : n <= m -> n < S m. Proof. apply Nat.lt_succ_r. Qed. +Register le_lt_n_Sm as num.nat.le_lt_n_Sm. + Hint Immediate lt_le_S: arith. Hint Immediate lt_n_Sm_le: arith. Hint Immediate le_lt_n_Sm: arith. @@ -99,6 +103,8 @@ Proof. apply Nat.succ_lt_mono. Qed. +Register lt_S_n as num.nat.lt_S_n. + Hint Resolve lt_n_Sn lt_S lt_n_S : arith. Hint Immediate lt_S_n : arith. @@ -133,6 +139,8 @@ Notation lt_trans := Nat.lt_trans (only parsing). Notation lt_le_trans := Nat.lt_le_trans (only parsing). Notation le_lt_trans := Nat.le_lt_trans (only parsing). +Register le_lt_trans as num.nat.le_lt_trans. + Hint Resolve lt_trans lt_le_trans le_lt_trans: arith. (** * Large = strict or equal *) diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index f12785029a..4657b7f46d 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -764,6 +764,9 @@ Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. Hint Unfold Nat.le : core. Hint Unfold Nat.lt : core. +Register Nat.le_trans as num.nat.le_trans. +Register Nat.nlt_0_r as num.nat.nlt_0_r. + (** [Nat] contains an [order] tactic for natural numbers *) (** Note that [Nat.order] is domain-agnostic: it will not prove diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 1c183930f9..c5a6651c05 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -34,6 +34,8 @@ Proof. intros a. apply (H (S (f a))). auto with arith. Defined. +Register well_founded_ltof as num.nat.well_founded_ltof. + Theorem well_founded_gtof : well_founded gtof. Proof. exact well_founded_ltof. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 149a7a0cc5..beb06ea912 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -159,6 +159,8 @@ Inductive le (n:nat) : nat -> Prop := where "n <= m" := (le n m) : nat_scope. +Register le_n as num.nat.le_n. + Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 998bbc7047..bd5185fdb0 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -32,11 +32,14 @@ Section Well_founded. Inductive Acc (x: A) : Prop := Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. + Register Acc as core.wf.acc. + Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. destruct 1; trivial. Defined. Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. + Register Acc_inv as core.wf.acc_inv. (** A relation is well-founded if every element is accessible *) |