Fixing test-suite

- bug in r15614: hnf was identity
- fix Print Assumptions
- bug in r15624: Dump glob of Print About only for Glob

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15630 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 14 insertions, 10 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f2f01c3f74..fa7ca0eb82 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -834,9 +834,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
       match reference_opt_value sigma env (destEvalRef constr) with
 	| Some c ->
 	    (match kind_of_term (strip_lam c) with
-              | CoFix _ | Fix _ -> s,[]
+              | CoFix _ | Fix _ -> s'
 	      | _ -> redrec (applist(c, stack)))
-	| None -> s,[]
+	| None -> s'
     else s'
   in applist (redrec c)
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 5e65bde250..31a42d132f 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -670,9 +670,10 @@ let print_opaque_name qid =
         let (_,c,ty) = lookup_named id env in
 	print_named_decl (id,c,ty)
 
-let print_about_any k =
+let print_about_any loc k =
   match k with
   | Term ref ->
+    Dumpglob.add_glob loc ref;
       pr_infos_list
        (print_ref false ref :: blankline ::
 	print_name_infos ref @
@@ -680,6 +681,9 @@ let print_about_any k =
 	print_opacity ref @
 	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->
+    let () = match Syntax_def.search_syntactic_definition kn with
+    | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref
+    | _ -> () in
       v 0 (
       print_syntactic_def kn ++ fnl () ++
       hov 0 (str "Expands to: " ++ pr_located_qualid k))
@@ -688,11 +692,11 @@ let print_about_any k =
 
 let print_about = function
   | ByNotation (loc,ntn,sc) ->
-      print_about_any
+      print_about_any loc
         (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
                ntn sc))
   | AN ref ->
-      print_about_any (locate_any_name ref)
+      print_about_any (loc_of_reference ref) (locate_any_name ref)
 
 (* for debug *)
 let inspect depth =
diff --git a/printing/printer.ml b/printing/printer.ml
index bae75011b7..a820f997a2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -612,7 +612,7 @@ let pr_assumptionset env s =
       opt_list (str "Axioms:") axioms;
       opt_list (str "Opaque constants:") opaque;
     ] in
-    prlist_with_sep fnl (pr_opt_no_spc (fun x -> x)) assums
+    prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
 let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7942a6da26..011818c15e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -420,7 +420,7 @@ let smart_global r =
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr;
     gr
 
-let dump_global r = 
+let dump_global r =
   let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
 
@@ -1372,9 +1372,9 @@ 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 -> 
-    dump_global qid; msg_notice (print_about qid)
-  | PrintImplicit qid -> 
+  | PrintAbout qid ->
+    msg_notice (print_about qid)
+  | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,r) ->
       (* Prints all the axioms and section variables used by a term *)