diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 85bb901046..fe896f9351 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) = | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc env sigma c) | ConstrTerm c when test c -> - h 0 (str "(" ++ prc env sigma c ++ str ")") + h (str "(" ++ prc env sigma c ++ str ")") | ConstrTerm c -> prc env sigma c @@ -1323,7 +1323,7 @@ let () = register_basic_print0 wit_smart_global (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var pr_lident pr_lident pr_id; + register_basic_print0 wit_hyp pr_lident pr_lident pr_id; register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"]; register_print0 wit_simple_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env; Genprint.register_print0 |