diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 1bdba699f7..80070a7493 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1307,7 +1307,6 @@ let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) let register_basic_print0 wit f g h = Genprint.register_print0 wit (lift f) (lift g) (lift_top h) - let pr_glob_constr_pptac env sigma c = pr_glob_constr_env env c |