diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /theories/Init/Peano.v | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'theories/Init/Peano.v')
-rw-r--r-- | theories/Init/Peano.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 3749baf6..6c4a6350 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -33,7 +33,6 @@ Open Scope nat_scope. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). -Hint Resolve eq_S: v62. Hint Resolve f_equal_nat: core. (** The predecessor function *) @@ -41,7 +40,6 @@ Hint Resolve f_equal_nat: core. Notation pred := Nat.pred (compat "8.4"). Definition f_equal_pred := f_equal pred. -Hint Resolve f_equal_pred: v62. Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. @@ -85,7 +83,6 @@ Notation plus := Nat.add (compat "8.4"). Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. -Hint Resolve f_equal2_plus: v62. Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). Hint Resolve f_equal2_nat: core. |