aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b74cd395a..e936fc40f 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -277,7 +277,7 @@ let _ =
| [VARG_CONSTR c] ->
(fun () ->
let (evmap,sign) = Command.get_current_context () in
- constr_display (Astterm.interp_constr evmap sign c))
+ constr_display (Constrintern.interp_constr evmap sign c))
| _ -> bad_vernac_args "PrintConstr")
let _ =
@@ -286,7 +286,7 @@ let _ =
| [VARG_CONSTR c] ->
(fun () ->
let (evmap,sign) = Command.get_current_context () in
- print_pure_constr (Astterm.interp_constr evmap sign c))
+ print_pure_constr (Constrintern.interp_constr evmap sign c))
| _ -> bad_vernac_args "PrintPureConstr")
*)