Imported Upstream version 8.5~beta1+dfsg

1 files changed, 19 insertions, 3 deletions

diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index deeb1f65..3c623346 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -6,9 +6,9 @@ Print eq_refl.
 About eq_refl.
 Print Implicit eq_refl.
 
-Print plus.
-About plus.
-Print Implicit plus.
+Print Nat.add.
+About Nat.add.
+Print Implicit Nat.add.
 
 About plus_n_O.
 
@@ -39,3 +39,19 @@ Print eq_refl.
 
 Arguments eq_refl {A} {x}, {A} x. (* Test new syntax *)
 Print eq_refl.
+
+
+Definition newdef := fun x:nat => x.
+
+Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
+  intros n h h'.
+  About n.                              (* search hypothesis *)
+  About h.                              (* search hypothesis *)
+Abort.
+
+Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False.
+  intros n g h h'.
+  About g.                              (* search hypothesis *)
+  About h.                              (* search hypothesis *)
+Abort.
+