About now accepts hypothesis names and goal selector.

1 files changed, 16 insertions, 0 deletions

diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index 4edeeb232c..3c623346bf 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -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.
+