diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml index c9aee7e92c1b51c43cbf988a36ac8425959ed223..99e31d81f6ac3292321a63b527eb9b8cd8cfa234 100644 --- a/src/kernel_services/ast_queries/logic_typing.ml +++ b/src/kernel_services/ast_queries/logic_typing.ml @@ -725,11 +725,6 @@ struct short_prefix: string; (* last '::' included *) } - let pp_scope fmt s = - Format.fprintf fmt "{ long: %S; short: %S }" - s.long_prefix s.short_prefix - [@@ warning "-32"] - let scopes : (scope option * scope list) Stack.t = Stack.create () let current_scope : scope option ref = ref None