aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
authorpboutill2012-07-20 14:22:40 +0000
committerpboutill2012-07-20 14:22:40 +0000
commitb78925e69d3e8b0ff2567bf0574e1bd55b33aa93 (patch)
treeef12e124ffef426bae708c94d9c2e4709fd6272a /printing/printer.ml
parent2285dae8af54043090ce5f8a59aa4162679714c6 (diff)
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
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml2
1 files changed, 1 insertions, 1 deletions
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 []