diff options
| author | Jim Fehrle | 2020-11-28 21:40:21 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-28 21:40:21 -0800 |
| commit | 54c12034bfb5fa8b1f83e14fb22f5b21398a7112 (patch) | |
| tree | ec1992ca2d514b40c7282d89786215989349245c /plugins/ltac | |
| parent | 9992bb15d4f90fc0cf3aa2854beb209bc5effac6 (diff) | |
Add missing print registration for wit_nat_or_var
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index fa5bbf7676..06c0a8fee3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1317,6 +1317,7 @@ let () = let pr_unit _ = str "()" in let open Genprint in register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_nat_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref pr_qualid (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_smart_global |