aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/prettyp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 37098e5042..f56f83e170 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -763,7 +763,7 @@ let print_opaque_name qid =
let ty = Universes.unsafe_type_of_global gr in
print_typed_value (mkConstruct cstr, ty)
| VarRef id ->
- lookup_named id env |> NamedDecl.set_id id |> print_named_decl
+ env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl
let print_about_any loc k =
match k with