aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-11-13 18:43:02 +0100
committerEmilio Jesus Gallego Arias2017-11-13 18:45:41 +0100
commitc571cdbbcac5cb4b4a5a19ab2f7ac51222316292 (patch)
tree2ec7070bc8d58ee4b6fd0734ea41964243a0f2ba /printing/printer.ml
parent6bd240fce21c172680a0cec5346b66e08c76418a (diff)
[api] Another large deprecation, `Nameops`
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 751e91cf05..075b03b7d1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -478,7 +478,7 @@ let pr_predicate pr_elt (b, elts) =
if List.is_empty elts then str"none" else pr_elts
let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
-let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p)
+let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p)
let pr_transparent_state (ids, csts) =
hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++