aboutsummaryrefslogtreecommitdiff
path: root/pretyping/recordops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/recordops.ml')
-rw-r--r--pretyping/recordops.ml2
1 files changed, 1 insertions, 1 deletions
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"