From 58f891c100d1a1821ed6385c1d06f9e0a77ecdac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 6 Nov 2018 09:30:45 +0100
Subject: Move debug term printer to kernel

---
 pretyping/recordops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.ml')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 5d74b59b27..4faa753dfb 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -270,7 +270,7 @@ let pr_cs_pattern = function
     Const_cs c -> Nametab.pr_global_env Id.Set.empty c
   | Prod_cs -> str "_ -> _"
   | Default_cs -> str "_"
-  | Sort_cs s -> Termops.pr_sort_family s
+  | Sort_cs s -> Sorts.pr_sort_family s
 
 let warn_redundant_canonical_projection =
   CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker"
-- 
cgit v1.2.3