7 files changed, 52 insertions, 20 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 05b741f0..1e6843d5 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -12,7 +12,6 @@ Set Implicit Arguments.
 
 Require Import Notations.
 Require Import Logic.
-Declare ML Module "nat_syntax_plugin".
 
 (********************************************************************)
 (** * Datatypes with zero and one element *)
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 57163b1b..1ff00ec1 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -42,10 +42,10 @@ Notation zero := (D0 Nil).
 
 Inductive int := Pos (d:uint) | Neg (d:uint).
 
-Delimit Scope uint_scope with uint.
-Bind Scope uint_scope with uint.
-Delimit Scope int_scope with int.
-Bind Scope int_scope with int.
+Delimit Scope dec_uint_scope with uint.
+Bind Scope dec_uint_scope with uint.
+Delimit Scope dec_int_scope with int.
+Bind Scope dec_int_scope with int.
 
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
@@ -161,3 +161,9 @@ with succ_double d :=
   end.
 
 End Little.
+
+(** Pseudo-conversion functions used when declaring
+    Numeral Notations on [uint] and [int]. *)
+
+Definition uint_of_uint (i:uint) := i.
+Definition int_of_int (i:int) := i.
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 15ca5abc..9d60cf54 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -29,6 +29,13 @@ Definition not (A:Prop) := A -> False.
 
 Notation "~ x" := (not x) : type_scope.
 
+(** Create the "core" hint database, and set its transparent state for
+  variables and constants explicitely. *)
+
+Create HintDb core.
+Hint Variables Opaque : core.
+Hint Constants Opaque : core.
+
 Hint Unfold not: core.
 
   (** [and A B], written [A /\ B], is the conjunction of [A] and [B]
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index ad1bc717..eb4ba0e5 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -24,6 +24,10 @@ Definition t := nat.
 
 (** ** Constants *)
 
+Local Notation "0" := O.
+Local Notation "1" := (S O).
+Local Notation "2" := (S (S O)).
+
 Definition zero := 0.
 Definition one := 1.
 Definition two := 2.
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index d5322d09..65e5e76a 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -31,6 +31,7 @@ Require Import Logic.
 Require Coq.Init.Nat.
 
 Open Scope nat_scope.
+Local Notation "0" := O.
 
 Definition eq_S := f_equal S.
 Definition f_equal_nat := f_equal (A:=nat).
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 802f18c0..6d98bcb3 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -19,9 +19,24 @@ Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
 Require Export Coq.Init.Tauto.
-(* Initially available plugins
-   (+ nat_syntax_plugin loaded in Datatypes) *)
+(* Some initially available plugins. See also:
+   - ltac_plugin (in Notations)
+   - tauto_plugin (in Tauto).
+*)
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
+Declare ML Module "numeral_notation_plugin".
+
+(* Parsing / printing of decimal numbers *)
+Arguments Nat.of_uint d%dec_uint_scope.
+Arguments Nat.of_int d%dec_int_scope.
+Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint
+  : dec_uint_scope.
+Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int
+  : dec_int_scope.
+
+(* Parsing / printing of [nat] numbers *)
+Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000).
+
 (* Default substrings not considered by queries like SearchAbout *)
 Add Search Blacklist "_subproof" "_subterm" "Private_".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index b6afba29..76632312 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -745,16 +745,16 @@ Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
 
-Notation sigS := sigT (compat "8.6").
-Notation existS := existT (compat "8.6").
-Notation sigS_rect := sigT_rect (compat "8.6").
-Notation sigS_rec := sigT_rec (compat "8.6").
-Notation sigS_ind := sigT_ind (compat "8.6").
-Notation projS1 := projT1 (compat "8.6").
-Notation projS2 := projT2 (compat "8.6").
-
-Notation sigS2 := sigT2 (compat "8.6").
-Notation existS2 := existT2 (compat "8.6").
-Notation sigS2_rect := sigT2_rect (compat "8.6").
-Notation sigS2_rec := sigT2_rec (compat "8.6").
-Notation sigS2_ind := sigT2_ind (compat "8.6").
+Notation sigS := sigT (compat "8.7").
+Notation existS := existT (compat "8.7").
+Notation sigS_rect := sigT_rect (compat "8.7").
+Notation sigS_rec := sigT_rec (compat "8.7").
+Notation sigS_ind := sigT_ind (compat "8.7").
+Notation projS1 := projT1 (compat "8.7").
+Notation projS2 := projT2 (compat "8.7").
+
+Notation sigS2 := sigT2 (compat "8.7").
+Notation existS2 := existT2 (compat "8.7").
+Notation sigS2_rect := sigT2_rect (compat "8.7").
+Notation sigS2_rec := sigT2_rec (compat "8.7").
+Notation sigS2_ind := sigT2_ind (compat "8.7").