diff options
| -rw-r--r-- | parsing/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 2f102488f5..447bb734a7 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -178,7 +178,7 @@ let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argu x) | ExtraArgType s -> try pi1 (Stringmap.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str " [no printer for " ++ str s ++ str "] " + with Not_found -> str "[no printer for " ++ str s ++ str "]" let rec pr_glob_generic prc prlc prtac x = @@ -223,7 +223,7 @@ let rec pr_glob_generic prc prlc prtac x = x) | ExtraArgType s -> try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x - with Not_found -> str "[no printer for " ++ str s ++ str "] " + with Not_found -> str "[no printer for " ++ str s ++ str "]" open Closure |