From a0281adfcaffa0c9c07df26fe239ed70f2ff06af Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 28 Nov 2020 21:40:21 -0800 Subject: [PATCH] Add missing print registration for wit_nat_or_var (cherry picked from commit 54c12034bfb5fa8b1f83e14fb22f5b21398a7112) --- plugins/ltac/pptactic.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index fa5bbf767642..06c0a8fee32a 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