diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-09 18:17:40 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-09 18:17:40 +0000 |
| commit | 06d096b3ff3dff8cca216091c0c5ffa3a7530e1d (patch) | |
| tree | d269a4777ecd906279d89140999753e816be33bb | |
| parent | 35dac4a85762924da7fb9b23f2029c2e5642a761 (diff) | |
Avoid a warning about unprintable new command Print Namespace
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15565 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | printing/ppvernac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d7b36d287..2d0173d19 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -909,6 +909,7 @@ let rec pr_vernac = function term *) | PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies") ++ spc() ++ pr_smart_global qid + | PrintNamespace dp -> str"Print Namespace" ++ pr_dirpath dp in pr_printable p | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr | VernacLocate loc -> |