Fix #11738 : Funind using deprecated Coqlib API.

5 files changed, 18 insertions, 0 deletions

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 *)