aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8bf86e9ef6..9541ea5882 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -952,5 +952,6 @@ let print_all_instances () =
let print_instances r =
let env = Global.env () in
- let inst = instances r in
+ let sigma = Evd.from_env env in
+ let inst = instances env sigma r in
prlist_with_sep fnl (pr_instance env) inst