5 files changed, 94 insertions, 34 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 6515b368d..152a722aa 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -10,7 +10,7 @@ fix F (t : t) : P t :=
 t_rect is monomorphic
 proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
-match eq_nat_dec x y with
+match Nat.eq_dec x y with
 | left eqprf => match eqprf in (_ = z) return (P z) with
                 | eq_refl => def
                 end
diff --git a/test-suite/output/Nametab.out b/test-suite/output/Nametab.out
index 1292123b1..c11621d7c 100644
--- a/test-suite/output/Nametab.out
+++ b/test-suite/output/Nametab.out
@@ -7,15 +7,15 @@ Constant Top.Q.N.K.foo
 Constant Top.Q.N.K.foo
 Constant Top.Q.N.K.foo
   (shorter name to refer to it in current context is Q.N.K.foo)
-Error: No module is referred to by basename K
-Error: No module is referred to by name N.K
+Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K)
+Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K)
 Module Top.Q.N.K
-Module Top.Q.N.K
-Error: No module is referred to by basename N
-Module Top.Q.N
+Module Top.Q.N.K (shorter name to refer to it in current context is Q.N.K)
+Module Top.Q.N (shorter name to refer to it in current context is Q.N)
 Module Top.Q.N
+Module Top.Q.N (shorter name to refer to it in current context is Q.N)
 Module Top.Q
-Module Top.Q
+Module Top.Q (shorter name to refer to it in current context is Q)
 Constant Top.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
 Constant Top.Q.N.K.foo
@@ -26,11 +26,11 @@ Constant Top.Q.N.K.foo
 Constant Top.Q.N.K.foo
   (shorter name to refer to it in current context is K.foo)
 Module Top.Q.N.K
-Error: No module is referred to by name N.K
-Module Top.Q.N.K
-Module Top.Q.N.K
-Error: No module is referred to by basename N
-Module Top.Q.N
+Module Top.Q.N.K (shorter name to refer to it in current context is K)
+Module Top.Q.N.K (shorter name to refer to it in current context is K)
+Module Top.Q.N.K (shorter name to refer to it in current context is K)
+Module Top.Q.N (shorter name to refer to it in current context is Q.N)
 Module Top.Q.N
+Module Top.Q.N (shorter name to refer to it in current context is Q.N)
 Module Top.Q
-Module Top.Q
+Module Top.Q (shorter name to refer to it in current context is Q)
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 253405b0f..08df91507 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -2,8 +2,11 @@ Axioms:
 foo : nat
 Axioms:
 foo : nat
-Fetching opaque proofs from disk for Coq.Arith.Plus
-Fetching opaque proofs from disk for Coq.Init.Peano
+Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZAdd
+Fetching opaque proofs from disk for Coq.Arith.PeanoNat
+Fetching opaque proofs from disk for Coq.Classes.Morphisms
+Fetching opaque proofs from disk for Coq.Init.Logic
+Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZBase
 Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 120c6a4ea..dbd72017a 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,7 +1,9 @@
 le_n: forall n : nat, n <= n
 le_S: forall n m : nat, n <= m -> n <= S m
-le_pred: forall n m : nat, n <= m -> pred n <= pred m
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
 le_S_n: forall n m : nat, S n <= S m -> n <= m
+le_0_n: forall n : nat, 0 <= n
+le_n_S: forall n m : nat, n <= m -> S n <= S m
 true: bool
 false: bool
 andb: bool -> bool -> bool
@@ -9,9 +11,15 @@ orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 xorb: bool -> bool -> bool
 negb: bool -> bool
+Nat.eqb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+Nat.testbit: nat -> nat -> bool
 eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_pred: forall x y : nat, x = y -> pred x = pred y
-pred_Sn: forall n : nat, n = pred (S n)
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+pred_Sn: forall n : nat, n = Nat.pred (S n)
 eq_add_S: forall n m : nat, S n = S m -> n = m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
@@ -23,7 +31,7 @@ f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
 mult_n_O: forall n : nat, 0 = n * 0
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> max n m = n
-max_r: forall n m : nat, n <= m -> max n m = m
-min_l: forall n m : nat, n <= m -> min n m = n
-min_r: forall n m : nat, m <= n -> min n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 6595302e1..ae37aaf32 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -5,28 +5,77 @@ orb: bool -> bool -> bool
 implb: bool -> bool -> bool
 xorb: bool -> bool -> bool
 negb: bool -> bool
+Nat.eqb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+Nat.testbit: nat -> nat -> bool
 O: nat
 S: nat -> nat
 length: forall A : Type, list A -> nat
-pred: nat -> nat
-plus: nat -> nat -> nat
-mult: nat -> nat -> nat
-minus: nat -> nat -> nat
-max: nat -> nat -> nat
-min: nat -> nat -> nat
+Nat.zero: nat
+Nat.one: nat
+Nat.two: nat
+Nat.succ: nat -> nat
+Nat.pred: nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.double: nat -> nat
+Nat.mul: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Nat.square: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.sqrt: nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2: nat -> nat
+Nat.div2: nat -> nat
+Nat.shiftl: nat -> nat -> nat
+Nat.shiftr: nat -> nat -> nat
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
 
 S: nat -> nat
-pred: nat -> nat
-plus: nat -> nat -> nat
-mult: nat -> nat -> nat
-minus: nat -> nat -> nat
-max: nat -> nat -> nat
-min: nat -> nat -> nat
+Nat.succ: nat -> nat
+Nat.pred: nat -> nat
+Nat.add: nat -> nat -> nat
+Nat.double: nat -> nat
+Nat.mul: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.div: nat -> nat -> nat
+Nat.modulo: nat -> nat -> nat
+Nat.gcd: nat -> nat -> nat
+Nat.square: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
+Nat.sqrt: nat -> nat
+Nat.log2_iter: nat -> nat -> nat -> nat -> nat
+Nat.log2: nat -> nat
+Nat.div2: nat -> nat
+Nat.shiftl: nat -> nat -> nat
+Nat.shiftr: nat -> nat -> nat
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+Nat.land: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.ldiff: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
 identity_refl: forall (A : Type) (a : A), identity a a
 iff_refl: forall A : Prop, A <-> A
 eq_refl: forall (A : Type) (x : A), x = x
+Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
 le_n: forall n : nat, n <= n
 pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
+Nat.divmod: nat -> nat -> nat -> nat -> nat * nat