About now accepts hypothesis names and goal selector.

6 files changed, 62 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index 5c1a27fa6f..1eca0a5185 100644
--- a/CHANGES
+++ b/CHANGES
@@ -52,11 +52,11 @@ Vernacular commands
 - Command "Search" has been renamed into "SearchHead". The command
   name "Search" now behaves like former "SearchAbout". The latter name
   is deprecated.
-- "Search" "SearchHead" "SearchRewrite" and "SearchPattern" now search
-  for hypothesis (of the current goal) first. They now also support the
-  goal selector prefix to specify another goal to search: e.g.
-  "n:Search id". This is also true for SearchAbout although it is
-  deprecated.
+- "Search" "About" "SearchHead" "SearchRewrite" and "SearchPattern"
+  now search for hypothesis (of the current goal by default) first.
+  They now also support the goal selector prefix to specify another
+  goal to search: e.g. "n:Search id". This is also true for
+  SearchAbout although it is deprecated.
 - The coq/user-contrib directory and the XDG directories are no longer
   recursively added to the load path, so files from installed libraries
   now need to be fully qualified for the "Require" command to find them.
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index f2a6309e38..bc167d94a3 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -74,7 +74,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation
+  | PrintAbout of reference or_by_notation*int option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3ae7bd92ca..ce731a5f54 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -794,7 +794,6 @@ GEXTEND Gram
       | IDENT "Print"; IDENT "Namespace" ; ns = dirpath ->
           VernacPrint (PrintNamespace ns)
       | IDENT "Inspect"; n = natural -> VernacPrint (PrintInspect n)
-      | IDENT "About"; qid = smart_global -> VernacPrint (PrintAbout qid)
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = ne_string ->
 	  VernacAddMLPath (false, dir)
@@ -839,6 +838,8 @@ GEXTEND Gram
       | IDENT "Check"; c = lconstr ->
 	 fun g -> VernacCheckMayEval (None, g, c)
       (* Searching the environment *)
+      | IDENT "About"; qid = smart_global ->
+	 fun g -> VernacPrint (PrintAbout (qid,g))
       | IDENT "SearchHead"; c = constr_pattern; l = in_or_out_modules ->
 	  fun g -> VernacSearch (SearchHead c,g, l)
       | IDENT "SearchPattern"; c = constr_pattern; l = in_or_out_modules ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2755b98c64..eca67ad86a 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -500,8 +500,9 @@ module Make
         keyword "Print Scope" ++ spc() ++ str s
       | PrintVisibility s ->
         keyword "Print Visibility" ++ pr_opt str s
-      | PrintAbout qid ->
-        keyword "About" ++ spc()  ++ pr_smart_global qid
+      | PrintAbout (qid,gopt) ->
+         pr_opt (fun g -> int g ++ str ":"++ spc()) gopt
+	 ++ keyword "About" ++ spc()  ++ pr_smart_global qid
       | PrintImplicit qid ->
         keyword "Print Implicit" ++ spc()  ++ pr_smart_global qid
       (* spiwack: command printing all the axioms and section variables used in a
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.
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 33428af027..e3b94a7776 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1528,6 +1528,39 @@ let vernac_global_check c =
   let env = Safe_typing.env_of_safe_env senv in
     msg_notice (print_safe_judgment env sigma j)
 
+
+let get_nth_goal n =
+  let pf = get_pftreestate() in
+  let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+  let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
+  gl
+  
+exception NoHyp
+(* Printing "About" information of a hypothesis of the current goal.
+   We only print the type and a small statement to this comes from the
+   goal. Precondition: there must be at least one current goal. *)
+let print_about_hyp_globs ref_or_by_not glnumopt =
+  try
+    let gl,id =
+      match glnumopt,ref_or_by_not with
+      | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *)
+	 (try get_nth_goal 1,id with _ -> raise NoHyp)
+      | Some n,AN (Ident (_loc,id)) ->  (* goal number given, catch if wong *)
+	 (try get_nth_goal n,id
+	  with
+	    Failure _ -> Errors.error ("No such goal: "^string_of_int n^"."))
+      | _ , _ -> raise NoHyp in
+    let hyps = pf_hyps gl in
+    let (id,bdyopt,typ) = Context.lookup_named id hyps in
+    let natureofid = match bdyopt with
+      | None -> "Hypothesis"
+      | Some bdy ->"Constant (let in)" in
+    v 0 (str (Id.to_string id) ++ str":" ++ pr_constr typ ++ fnl() ++ fnl()
+	 ++ str natureofid ++ str " of the goal context.")
+  with (* fallback to globals *)
+    | NoHyp | Not_found -> print_about ref_or_by_not
+
+	       
 let vernac_print = function
   | PrintTables -> msg_notice (print_tables ())
   | PrintFullContext-> msg_notice (print_full_context_typ ())
@@ -1568,8 +1601,8 @@ let vernac_print = function
       msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
-  | PrintAbout qid ->
-    msg_notice (print_about qid)
+  | PrintAbout (ref_or_by_not,glnumopt) ->
+     msg_notice (print_about_hyp_globs ref_or_by_not glnumopt)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->